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
x✝ : p ∨ q ∧ r
⊢ (p ∨ q) ∧ (p ∨ r)
no goals