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:
have ⟨np, nq⟩ := h
State after:
p q : Prop
h : ¬p ∧ ¬q
np : ¬p
nq : ¬q
⊢ ¬(p ∨ q)

State before:
p q : Prop
h : ¬p ∧ ¬q
np : ¬p
nq : ¬q
⊢ ¬(p ∨ q)
Tactic:
exact match Classical.em p, Classical.em q with
| Or.inl pp,  _   => False.elim (np pp)
| _        ,  Or.inl pq  => False.elim (nq pq)
| Or.inr npp, Or.inr npq => λ h₂ =>
                               match h₂ with
                               | Or.inl pp => False.elim (npp pp)
                               | Or.inr pq => False.elim (npq pq)
State after:
no goals