have : p ∨ r := Or.inr ‹r›
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)