intro
| ⟨u, v, ⟨u1, u2, pu1, pu2, pu⟩, pv, px⟩ =>
  rw [pu, Word.monoid.mul_assoc u1 u2 v] at px
  exact ⟨ u1, u2 * v, pu1, ⟨u2, v, pu2, pv, rfl⟩, px ⟩
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)
no goals