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

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

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

State before:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ ¬c ∨ a
Tactic:
have hite' := notNotElim hite
State after:
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a

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

State before:
c a b : Prop
h : Decidable c
h✝ : c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a
Tactic:
exact Or.inr hite'
State after:
no goals

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