cases h with
| inl hpq =>
  constructor
  exact hpq.1
  apply Or.inl
  exact hpq.2
  | inr hpr =>
  constructor
  exact hpr.1
  apply Or.inr
  exact hpr.2
P Q R : Prop
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)
no goals