. intro
  | ⟨u,v,h1,h2,h3⟩ =>
    cases h2 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 ∘ₗ L2 ∪ L1 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)
case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3 → w ∈ L1 ∘ₗ (L2 ∪ L3)