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