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
left✝ : p ∨ q
right✝ : p ∨ r
⊢ p ∨ q ∧ r
no goals