{ intro hnor
  constructor
  { intro hp
    exact hnor (Or.inl hp)
  }
  { intro hq
    exact hnor (Or.inr hq)
  }
}
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)