∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M],
  FreeMonoid.lift =
    {
      toFun := fun f =>
        { toFun := fun l => FreeMonoid.prodAux (List.map f (FreeMonoid.toList l)), map_one' := ⋯, map_mul' := ⋯ },
      invFun := fun f x => f (FreeMonoid.of x), left_inv := ⋯, right_inv := ⋯ }