Theorem: Smt.Reconstruct.Builtin.notIteElim1 (Smt/Reconstruct/Builtin/Lemmas.lean)

State before:
c a b : Prop
hc : Decidable c
⊢ (¬if c then a else b) → ¬c ∨ ¬a
Tactic:
intros h
State after:
c a b : Prop
hc : Decidable c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a

State before:
c a b : Prop
hc : Decidable c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
cases hc with
| isTrue hc   => exact Or.inr h
| isFalse hnc => exact Or.inl hnc
State after:
no goals

State before:
case isTrue
c a b : Prop
hc : c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
exact Or.inr h
State after:
no goals

State before:
case isFalse
c a b : Prop
hnc : ¬c
h : ¬if c then a else b
⊢ ¬c ∨ ¬a
Tactic:
exact Or.inl hnc
State after:
no goals