rw [<- Word.monoid.mul_assoc] at this
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * (w * x) ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
this : u * w * x ∈ L ↔ v * w * x ∈ L
⊢ u * w * x ∈ L ↔ v * w * x ∈ L