case mp =>
  intro h
  have _ : P := h.left
  cases h.right with
  | inl hq => apply Or.inl; constructor <;> assumption
  | inr rq => apply Or.inr; constructor <;> assumption
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
no goals