{ intro hnand
  by_cases p 
  { exact Or.inr λ hq => hnand ⟨h, hq⟩}
  { left
    exact h
  }
}
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)