Theorem: Smt.Reconstruct.Prop.deMorganSmall₃ (Smt/Reconstruct/Prop/Lemmas.lean)

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

State before:
p q : Prop
h : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
Tactic:
match Classical.em p, Classical.em q with
| Or.inl hp, Or.inl hq  => exact False.elim (h (And.intro hp hq))
| _,         Or.inr hnq => exact Or.inr hnq
| Or.inr hnp, _        => exact Or.inl hnp
State after:
no goals

State before:
p q : Prop
h : ¬(p ∧ q)
hp : p
hq : q
⊢ ¬p ∨ ¬q
Tactic:
exact False.elim (h (And.intro hp hq))
State after:
no goals

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

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