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