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