[GOAL]
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
⊢ ∀ (x y : FreeMonoid α),
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
          x *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
        map_one' :=
          (_ :
            (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldl f) (↑FreeMonoid.toList xs))) 1) }
        y✝
[PROOFSTEP]
simp only [FreeMonoid.toList_mul, flip, unop_op, List.foldl_append, op_inj]
[GOAL]
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ (op fun a => List.foldl f (List.foldl f a (↑FreeMonoid.toList x✝)) (↑FreeMonoid.toList y✝)) =
    (op fun a => List.foldl f a (↑FreeMonoid.toList x✝)) * op fun a => List.foldl f a (↑FreeMonoid.toList y✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
⊢ ∀ (x y : FreeMonoid α),
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          x *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
        map_one' :=
          (_ :
            (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        y✝
[PROOFSTEP]
apply unop_injective
[GOAL]
case a
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ unop
      (OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        (x✝ * y✝)) =
    unop
      (OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          y✝)
[PROOFSTEP]
funext
[GOAL]
case a.h
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ unop
      (OneHom.toFun
        { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
          map_one' :=
            (_ :
              (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
        (x✝¹ * y✝))
      x✝ =
    unop
      (OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          x✝¹ *
        OneHom.toFun
          { toFun := fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs)),
            map_one' :=
              (_ :
                (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1 =
                  (fun xs => op (flip (List.foldlM f) (↑FreeMonoid.toList xs))) 1) }
          y✝)
      x✝
[PROOFSTEP]
apply List.foldlM_append
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
⊢ ∀ (x y : FreeMonoid α),
    OneHom.toFun
        { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
          map_one' :=
            (_ :
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          x *
        OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝ y✝ : FreeMonoid α
⊢ OneHom.toFun
      { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
        map_one' :=
          (_ :
            (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
          map_one' :=
            (_ :
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
          map_one' :=
            (_ :
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
        y✝
[PROOFSTEP]
funext
[GOAL]
case h
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ OneHom.toFun
      { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
        map_one' :=
          (_ :
            (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
              (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
      (x✝¹ * y✝) x✝ =
    (OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          x✝¹ *
        OneHom.toFun
          { toFun := fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs),
            map_one' :=
              (_ :
                (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1 =
                  (fun xs => flip (List.foldrM f) (↑FreeMonoid.toList xs)) 1) }
          y✝)
      x✝
[PROOFSTEP]
apply List.foldrM_append
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 : Type ?u.11080} (x : α_1), (fun x => ↑f) α_1 (pure x) = pure x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ : Type ?u.11080
x✝ : α✝
⊢ (fun x => ↑f) α✝ (pure x✝) = pure x✝
[PROOFSTEP]
simp only [map_one, pure]
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 β_1 : Type ?u.11080} (x : Const α (α_1 → β_1)) (y : Const α α_1),
    (fun x => ↑f) β_1 (Seq.seq x fun x => y) = Seq.seq ((fun x => ↑f) (α_1 → β_1) x) fun x => (fun x => ↑f) α_1 y
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ β✝ : Type ?u.11080
x✝ : Const α (α✝ → β✝)
y✝ : Const α α✝
⊢ (fun x => ↑f) β✝ (Seq.seq x✝ fun x => y✝) = Seq.seq ((fun x => ↑f) (α✝ → β✝) x✝) fun x => (fun x => ↑f) α✝ y✝
[PROOFSTEP]
simp only [Seq.seq, map_mul]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
⊢ ↑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = foldlM.mk ∘ flip f
[PROOFSTEP]
ext1 x
[GOAL]
case h
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (↑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip f) x
[PROOFSTEP]
simp [(· ∘ ·), foldlM.ofFreeMonoid, foldlM.mk, flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
⊢ ↑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = foldrM.mk ∘ f
[PROOFSTEP]
ext
[GOAL]
case h
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
x✝ : β
⊢ (↑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of) x✝ = (foldrM.mk ∘ f) x✝
[PROOFSTEP]
simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (foldMap FreeMonoid.of xs) =
    ↑FreeMonoid.toList (List.reverse (List.reverse (foldMap FreeMonoid.of xs)))
[PROOFSTEP]
simp only [List.reverse_reverse]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (List.reverse (List.reverse (foldMap FreeMonoid.of xs))) =
    ↑FreeMonoid.toList (List.reverse (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs))))
[PROOFSTEP]
simp only [List.foldr_eta]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ↑FreeMonoid.toList (List.reverse (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs)))) =
    List.reverse (unop (↑(Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) [])
[PROOFSTEP]
simp [flip, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ List.reverse (unop (↑(Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []) = toList xs
[PROOFSTEP]
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ List.reverse (unop (foldMap (↑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []) = toList xs
[PROOFSTEP]
simp only [toList, foldl, List.reverse_inj, Foldl.get, foldl.ofFreeMonoid_comp_of, Function.comp_apply]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs
[PROOFSTEP]
simp only [foldMap, traverse_map, Function.comp]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)
[PROOFSTEP]
rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = unop (↑(Foldl.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x
[PROOFSTEP]
simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get, FreeMonoid.ofList_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)
[PROOFSTEP]
change _ = Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs) _
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = ↑(Foldr.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
[PROOFSTEP]
rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free, foldr.ofFreeMonoid_comp_of]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β
xs : t α
⊢ toList (f <$> xs) = f <$> toList xs
[PROOFSTEP]
simp only [toList_spec, Free.map_eq_map, foldMap_hom, foldMap_map, FreeMonoid.ofList_toList, FreeMonoid.map_of, (· ∘ ·)]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : α → γ → α
a : α
l : t β
⊢ foldl f a (g <$> l) = foldl (fun x y => f x (g y)) a l
[PROOFSTEP]
simp only [foldl, foldMap_map, (· ∘ ·), flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : γ → α → α
a : α
l : t β
⊢ foldr f a (g <$> l) = foldr (f ∘ g) a l
[PROOFSTEP]
simp only [foldr, foldMap_map, (· ∘ ·), flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : List α
⊢ toList xs = xs
[PROOFSTEP]
simp only [toList_spec, foldMap, traverse]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : List α
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
[PROOFSTEP]
induction xs
[GOAL]
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
case nil => rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
[PROOFSTEP]
case nil => rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
case cons _ _ ih => conv_rhs => rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
case cons _ _ ih => conv_rhs => rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
conv_rhs => rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝
[PROOFSTEP]
rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝
[PROOFSTEP]
rw [← ih]; rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝
[PROOFSTEP]
rw [← ih]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ length xs = List.length (toList xs)
[PROOFSTEP]
unfold length
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = List.length (toList xs)
[PROOFSTEP]
rw [foldl_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = List.length (toList xs)
[PROOFSTEP]
generalize toList xs = ys
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys
[PROOFSTEP]
rw [← Nat.add_zero ys.length]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = List.length ys + 0
[PROOFSTEP]
generalize 0 = n
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } ys).down = List.length ys + n
[PROOFSTEP]
induction' ys with _ _ ih generalizing n
[GOAL]
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n✝ n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } []).down = List.length [] + n
[PROOFSTEP]
simp
[GOAL]
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n✝ : ℕ
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = List.length tail✝ + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down =
    List.length (head✝ :: tail✝) + n
[PROOFSTEP]
simp_arith [ih]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ foldlm f x xs = unop (↑(foldlM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x
[PROOFSTEP]
simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f), foldlm.ofFreeMonoid_comp_of, foldlM.get,
  FreeMonoid.ofList_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ unop (↑(foldlM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs))) x = List.foldlM f x (toList xs)
[PROOFSTEP]
simp [foldlM.ofFreeMonoid, unop_op, flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = List.foldrM f x (toList xs)
[PROOFSTEP]
change _ = foldrM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs) x
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = ↑(foldrM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
[PROOFSTEP]
simp only [foldrm, toList_spec, foldMap_hom_free (foldrM.ofFreeMonoid f), foldrm.ofFreeMonoid_comp_of, foldrM.get,
  FreeMonoid.ofList_toList]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : α → γ → m α
a : α
l : t β
⊢ foldlm f a (g <$> l) = foldlm (fun x y => f x (g y)) a l
[PROOFSTEP]
simp only [foldlm, foldMap_map, (· ∘ ·), flip]
[GOAL]
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : γ → α → m α
a : α
l : t β
⊢ foldrm f a (g <$> l) = foldrm (f ∘ g) a l
[PROOFSTEP]
simp only [foldrm, foldMap_map, (· ∘ ·), flip]
