intro
| ⟨u,v,h1,h2,h3⟩ =>
  cases h1 with
  | inl hl => apply Or.inl; exists u; exists v
  | inr hr => apply Or.inr; exists u; exists v
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 → w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
no goals