exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
α : Type u_1
X Y Z : Language α
x : Word α
x✝ : x ∈ X ∘ₗ Y ∘ₗ Z
u v u1 u2 : Word α
pu1 : u1 ∈ X
pu2 : u2 ∈ Y
pu : u = u1 * u2
pv : v ∈ Z
px : x = u1 * (u2 * v)
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z)
no goals