cases pu with | intro v pv =>
match pv with
| ⟨h1, h2, h3⟩ => exists u, v; exact ⟨h1, Or.inr h2, h3⟩
case intro
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u : Word α
pu : ∃ v, u ∈ L1 ∧ v ∈ L3 ∧ w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
no goals