nelsmartin

import Lean

open Lean Lean.Expr Lean.Meta Lean.Elab.Tactic
set_option linter.unusedVariables false
/-
**Tactic Scope** (I belive)
If a (provable) theorem involves only `And`, `→`, `↔`, `False`, and variables of type `Prop`, then there exists a choice from the options presented by `so` that will solve the theorem.

The tactic will show options related to:
1. Splitting the goal with Iff.intro

nelsmartin

import Lean

open Lean Lean.Expr Lean.Meta Lean.Elab.Tactic
set_option linter.unusedVariables false

/-
Usage:
Use `so` (short for show_options) at each step in the proof to see what the possible next moves are, as well the proof state that would result from using the given tactic.
-/