cases h with
| inl h₁ => exact Or.inl (Or.inl h₁)
| inr h₂ => cases h₂ with
            | inl h₃ => exact Or.inl (Or.inr h₃)
            | inr h₄ => exact Or.inr h₄
P Q R : Prop
h : P ∨ Q ∨ R
⊢ (P ∨ Q) ∨ R
no goals