case mpr =>
  intro (And.intro (_ : ¬p) (_ : ¬q)) (_ : p ∨ q)
  show False
  match ‹p ∨ q› with
  | Or.inl (_ : p) => exact absurd ‹p› ‹¬p›
  | Or.inr (_ : q) => exact absurd ‹q› ‹¬q›
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
no goals