Theorem: Smt.Reconstruct.Prop.cnfImpliesNeg2 (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {p q : Prop}, (p → q) ∨ ¬q
Tactic:
intros p q
State after:
p q : Prop
⊢ (p → q) ∨ ¬q

State before:
p q : Prop
⊢ (p → q) ∨ ¬q
Tactic:
apply orComm
State after:
case a
p q : Prop
⊢ ¬q ∨ (p → q)

State before:
case a
p q : Prop
⊢ ¬q ∨ (p → q)
Tactic:
apply orImplies
State after:
case a.a
p q : Prop
⊢ ¬¬q → p → q

State before:
case a.a
p q : Prop
⊢ ¬¬q → p → q
Tactic:
intros hnnq _
State after:
case a.a
p q : Prop
hnnq : ¬¬q
a✝ : p
⊢ q

State before:
case a.a
p q : Prop
hnnq : ¬¬q
a✝ : p
⊢ q
Tactic:
exact notNotElim hnnq
State after:
no goals