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:
exact match Classical.em p, Classical.em q with
| Or.inl pp,  _          => False.elim (h (Or.inl pp))
| Or.inr _,   Or.inl pq  => False.elim (h (Or.inr pq))
| Or.inr npp, Or.inr npq => And.intro npp npq
State after:
no goals