[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
xs : List (FreeMonoid α)
⊢ ↑toList (List.prod xs) = List.join (List.map (↑toList) xs)
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
⊢ ↑toList (List.prod []) = List.join (List.map ↑toList [])
[PROOFSTEP]
simp [*, List.join]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
head✝ : FreeMonoid α
tail✝ : List (FreeMonoid α)
tail_ih✝ : ↑toList (List.prod tail✝) = List.join (List.map (↑toList) tail✝)
⊢ ↑toList (List.prod (head✝ :: tail✝)) = List.join (List.map (↑toList) (head✝ :: tail✝))
[PROOFSTEP]
simp [*, List.join]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
xs : List (List α)
⊢ ↑toList (↑ofList (List.join xs)) = ↑toList (List.prod (List.map (↑ofList) xs))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
f g : FreeMonoid α →* M
h : ∀ (x : α), ↑f (of x) = ↑g (of x)
l : FreeMonoid α
x : α
xs : FreeMonoid α
hxs : ↑f xs = ↑g xs
⊢ ↑f (of x * xs) = ↑g (of x * xs)
[PROOFSTEP]
simp only [h, hxs, MonoidHom.map_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
f : α → M
x✝¹ x✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun l => prodAux (List.map f (↑toList l)),
        map_one' :=
          (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
      (x✝¹ * x✝) =
    OneHom.toFun
        { toFun := fun l => prodAux (List.map f (↑toList l)),
          map_one' :=
            (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
        x✝¹ *
      OneHom.toFun
        { toFun := fun l => prodAux (List.map f (↑toList l)),
          map_one' :=
            (_ : (fun l => prodAux (List.map f (↑toList l))) 1 = (fun l => prodAux (List.map f (↑toList l))) 1) }
        x✝
[PROOFSTEP]
simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ MonoidHom.comp g (↑lift f) = ↑lift (↑g ∘ f)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
x✝ : α
⊢ ↑(MonoidHom.comp g (↑lift f)) (of x✝) = ↑(↑lift (↑g ∘ f)) (of x✝)
[PROOFSTEP]
simp
