. intro
  | ⟨u, v, pu, ⟨v1, v2, pv1, pv2, pv⟩, px⟩ =>
    rw [pv, <- Word.monoid.mul_assoc u v1 v2] at px
    exact ⟨ u * v1, v2, ⟨u, v1, pu, pv1, rfl⟩, pv2, px ⟩
case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z
no goals