exists u, v
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3)
α : Type u_1
L1 L2 L3 : Language α
w : Word α
x✝ : w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
u v : Word α
pv : u ∈ L1 ∧ v ∈ L2 ∧ w = u * v
h1 : u ∈ L1
h2 : v ∈ L2
h3 : w = u * v
⊢ u ∈ L1 ∧ v ∈ L2 ∪ L3 ∧ w = u * v