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