Theorem: Word_mul (Bruhat/Word.lean)

State before:
w v : Word
⊢ Word.toPerm (w ++ v) = Word.toPerm w * Word.toPerm v
Tactic:
simp only [Word.toPerm, FreeMonoid.ofList_append, map_mul, FreeMonoid.lift_ofList]
State after:
no goals