case mpr =>
  intro h
  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
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
no goals