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

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

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

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

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

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