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

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

State before:
p q : Prop
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
match Classical.em p, Classical.em q with
| _,         Or.inl hq  => exact Or.inr (Or.inr hq)
| Or.inl hp, Or.inr hnq => apply Or.inl
                           intro f
                           exact absurd (f hp) hnq
| Or.inr hnp, _         => exact Or.inr (Or.inl hnp)
State after:
no goals

State before:
p q : Prop
x✝ : p ∨ ¬p
hq : q
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
exact Or.inr (Or.inr hq)
State after:
no goals

State before:
p q : Prop
hp : p
hnq : ¬q
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
apply Or.inl
State after:
case h
p q : Prop
hp : p
hnq : ¬q
⊢ ¬(p → q)

State before:
case h
p q : Prop
hp : p
hnq : ¬q
⊢ ¬(p → q)
Tactic:
intro f
State after:
case h
p q : Prop
hp : p
hnq : ¬q
f : p → q
⊢ False

State before:
case h
p q : Prop
hp : p
hnq : ¬q
f : p → q
⊢ False
Tactic:
exact absurd (f hp) hnq
State after:
no goals

State before:
p q : Prop
hnp : ¬p
x✝ : q ∨ ¬q
⊢ ¬(p → q) ∨ ¬p ∨ q
Tactic:
exact Or.inr (Or.inl hnp)
State after:
no goals