have : ¬q := by
  intro (_ : q)
  show False
  have : p ∨ q := Or.inr ‹q›
  exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬p ∧ ¬q
p q : Prop
x✝ : ¬(p ∨ q)
this✝ : ¬p
this : ¬q
⊢ ¬p ∧ ¬q