[GOAL]
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x : FreeMagma α
⊢ ∀ (x y : FreeMagma α), ↑f x = ↑g x → ↑f y = ↑g y → ↑f (x * y) = ↑g (x * y)
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : ↑f x✝ = ↑g x✝
a✝ : ↑f y✝ = ↑g y✝
⊢ ↑f (x✝ * y✝) = ↑g (x✝ * y✝)
[PROOFSTEP]
simp only [map_mul, *]
[GOAL]
α : Type u
β : Type v
inst✝ : Mul β
f✝ f : α → β
⊢ (fun F => ↑F ∘ of)
      ((fun f => { toFun := liftAux f, map_mul' := (_ : ∀ (x y : FreeMagma α), liftAux f (x * y) = liftAux f (x * y)) })
        f) =
    f
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : Mul β
f : α → β
F : FreeMagma α →ₙ* β
⊢ (fun f => { toFun := liftAux f, map_mul' := (_ : ∀ (x y : FreeMagma α), liftAux f (x * y) = liftAux f (x * y)) })
      ((fun F => ↑F ∘ of) F) =
    F
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u
β : Type v
inst✝ : Mul β
f : α → β
F : FreeMagma α →ₙ* β
x✝ : α
⊢ (↑((fun f => { toFun := liftAux f, map_mul' := (_ : ∀ (x y : FreeMagma α), liftAux f (x * y) = liftAux f (x * y)) })
            ((fun F => ↑F ∘ of) F)) ∘
        of)
      x✝ =
    (↑F ∘ of) x✝
[PROOFSTEP]
rfl
[GOAL]
α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ id <$> (x * y) = x * y
[PROOFSTEP]
rw [map_mul', ih1, ih2]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x => f x >>= g
ih2 : y >>= f >>= g = y >>= fun x => f x >>= g
⊢ x * y >>= f >>= g = x * y >>= fun x => f x >>= g
[PROOFSTEP]
rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = x
ih2 : traverse pure y = y
⊢ traverse pure (x * y) = x * y
[PROOFSTEP]
rw [traverse_mul, ih1, ih2, mul_map_seq]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeMagma α✝
x : α✝
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
[PROOFSTEP]
simp only [(· ∘ ·), traverse_pure, traverse_pure', functor_norm]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (x * y) = Functor.Comp.mk (traverse f <$> traverse g (x * y))
[PROOFSTEP]
rw [traverse_mul, ih1, ih2, traverse_mul]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (Seq.seq ((fun x x_1 => x * x_1) <$> Functor.Comp.mk (traverse f <$> traverse g x)) fun x =>
      Functor.Comp.mk (traverse f <$> traverse g y)) =
    Functor.Comp.mk (traverse f <$> Seq.seq ((fun x x_1 => x * x_1) <$> traverse g x) fun x => traverse g y)
[PROOFSTEP]
simp [Functor.Comp.map_mk, Functor.map_map, (· ∘ ·), Comp.seq_mk, seq_map_assoc, map_seq, traverse_mul]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = id.mk (f <$> x)
ih2 : traverse (pure ∘ f) y = id.mk (f <$> y)
⊢ traverse (pure ∘ f) (x * y) = id.mk (f <$> (x * y))
[PROOFSTEP]
rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = id.mk (f <$> x)
ih2 : traverse (pure ∘ f) y = id.mk (f <$> y)
⊢ id.mk (f <$> x) * id.mk (f <$> y) = id.mk (f <$> x * f <$> y)
[PROOFSTEP]
rfl
[GOAL]
α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ : FreeMagma α
x : α
⊢ (fun {α} => ApplicativeTransformation.app η α) (traverse f (pure x)) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (pure x)
[PROOFSTEP]
simp only [traverse_pure, functor_norm, Function.comp_apply]
[GOAL]
α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
src✝ : LawfulMonad FreeMagma := instLawfulMonadFreeMagma
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ x y : FreeMagma α
ih1 :
  (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
ih2 :
  (fun {α} => ApplicativeTransformation.app η α) (traverse f y) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) y
⊢ (fun {α} => ApplicativeTransformation.app η α) (traverse f (x * y)) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x * y)
[PROOFSTEP]
simp only [traverse_mul, functor_norm, ih1, ih2]
[GOAL]
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ AssocQuotient α
[PROOFSTEP]
refine' Quot.liftOn₂ x y (fun x y ↦ Quot.mk _ (x * y)) _ _
[GOAL]
case refine'_1
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a b₁ b₂ : α),
    AssocRel α b₁ b₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a b₁ = (fun x y => Quot.mk (AssocRel α) (x * y)) a b₂
[PROOFSTEP]
rintro a b₁ b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩)
[GOAL]
case refine'_1.intro
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e : α
⊢ (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * d * e) = (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * e))
[PROOFSTEP]
simp only
[GOAL]
case refine'_1.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e f : α
⊢ (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * e * f)) =
    (fun x y => Quot.mk (AssocRel α) (x * y)) a (c * (d * (e * f)))
[PROOFSTEP]
simp only
[GOAL]
case refine'_1.intro
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e : α
⊢ Quot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e)))
[PROOFSTEP]
exact quot_mk_assoc_left _ _ _ _
[GOAL]
case refine'_1.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e f : α
⊢ Quot.mk (AssocRel α) (a * (c * (d * e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
[PROOFSTEP]
rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]
[GOAL]
case refine'_2
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a₁ a₂ b : α),
    AssocRel α a₁ a₂ → (fun x y => Quot.mk (AssocRel α) (x * y)) a₁ b = (fun x y => Quot.mk (AssocRel α) (x * y)) a₂ b
[PROOFSTEP]
rintro a₁ a₂ b (⟨c, d, e⟩ | ⟨c, d, e, f⟩)
[GOAL]
case refine'_2.intro
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e : α
⊢ (fun x y => Quot.mk (AssocRel α) (x * y)) (c * d * e) b = (fun x y => Quot.mk (AssocRel α) (x * y)) (c * (d * e)) b
[PROOFSTEP]
simp only
[GOAL]
case refine'_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ (fun x y => Quot.mk (AssocRel α) (x * y)) (c * (d * e * f)) b =
    (fun x y => Quot.mk (AssocRel α) (x * y)) (c * (d * (e * f))) b
[PROOFSTEP]
simp only
[GOAL]
case refine'_2.intro
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e : α
⊢ Quot.mk (AssocRel α) (c * d * e * b) = Quot.mk (AssocRel α) (c * (d * e) * b)
[PROOFSTEP]
simp only [quot_mk_assoc, quot_mk_assoc_left]
[GOAL]
case refine'_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
[PROOFSTEP]
rw [quot_mk_assoc, quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc_left, quot_mk_assoc_left, ← quot_mk_assoc c d, ←
  quot_mk_assoc c d, quot_mk_assoc_left]
[GOAL]
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝ f : α →ₙ* β
x : AssocQuotient α
⊢ ∀ (a b : α), AssocRel α a b → ↑f a = ↑f b
[PROOFSTEP]
rintro a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩)
[GOAL]
case intro
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝ f : α →ₙ* β
x : AssocQuotient α
c d e : α
⊢ ↑f (c * d * e) = ↑f (c * (d * e))
[PROOFSTEP]
simp only [map_mul, mul_assoc]
[GOAL]
case left
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝¹ f✝ : α →ₙ* β
x : AssocQuotient α
c d e f : α
⊢ ↑f✝ (c * (d * e * f)) = ↑f✝ (c * (d * (e * f)))
[PROOFSTEP]
simp only [map_mul, mul_assoc]
[GOAL]
α : Type u
x y : FreeSemigroup α
⊢ length (x * y) = length x + length y
[PROOFSTEP]
simp [length, ← add_assoc, add_right_comm, List.length, List.length_append]
[GOAL]
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeSemigroup α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : ↑f (of x) = ↑g (of x)
hy : ↑f y = ↑g y
⊢ ↑f (of x * y) = ↑g (of x * y)
[PROOFSTEP]
simp only [map_mul, *]
[GOAL]
α : Type u
β : Type v
inst✝ : Semigroup β
f✝ f : α → β
x y : FreeSemigroup α
⊢ (fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail) (x * y) =
    (fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail) x *
      (fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail) y
[PROOFSTEP]
simp only [head_mul, tail_mul, ← List.foldl_map f, List.foldl_append, List.foldl_cons, List.foldl_assoc]
[GOAL]
α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ ↑(↑lift f) (of x * y) = f x * ↑(↑lift f) y
[PROOFSTEP]
rw [map_mul, lift_of]
[GOAL]
α : Type u
β : Type v
f : α → β
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : length (↑(map f) (of x)) = length (of x)
hy : length (↑(map f) y) = length y
⊢ length (↑(map f) (of x * y)) = length (of x * y)
[PROOFSTEP]
simp only [map_mul, length_mul, *]
[GOAL]
α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ id <$> (pure x * y) = pure x * y
[PROOFSTEP]
rw [map_mul', ih1, ih2]
[GOAL]
α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x => g x >>= f
ih2 : y >>= g >>= f = y >>= fun x => g x >>= f
⊢ pure x * y >>= g >>= f = pure x * y >>= fun x => g x >>= f
[PROOFSTEP]
rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      Seq.seq ((fun x x_1 => x * x_1) <$> traverse F { head := x, tail := tl }) fun x =>
        traverse F { head := y, tail := L2 }
x : α
⊢ (Seq.seq ((fun x x_1 => x * x_1) <$> pure <$> F x) fun x =>
      traverse F ({ head := hd, tail := tl } * { head := y, tail := L2 })) =
    Seq.seq
      ((fun x x_1 => x * x_1) <$>
        Seq.seq ((fun x x_1 => x * x_1) <$> pure <$> F x) fun x => traverse F { head := hd, tail := tl })
      fun x => traverse F { head := y, tail := L2 }
[PROOFSTEP]
rw [ih]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      Seq.seq ((fun x x_1 => x * x_1) <$> traverse F { head := x, tail := tl }) fun x =>
        traverse F { head := y, tail := L2 }
x : α
⊢ (Seq.seq ((fun x x_1 => x * x_1) <$> pure <$> F x) fun x =>
      Seq.seq ((fun x x_1 => x * x_1) <$> traverse F { head := hd, tail := tl }) fun x =>
        traverse F { head := y, tail := L2 }) =
    Seq.seq
      ((fun x x_1 => x * x_1) <$>
        Seq.seq ((fun x x_1 => x * x_1) <$> pure <$> F x) fun x => traverse F { head := hd, tail := tl })
      fun x => traverse F { head := y, tail := L2 }
[PROOFSTEP]
simp only [(· ∘ ·), (mul_assoc _ _ _).symm, functor_norm]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = of x
ih2 : traverse pure y = y
⊢ traverse pure (of x * y) = of x * y
[PROOFSTEP]
rw [traverse_mul, ih1, ih2, mul_map_seq]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
[PROOFSTEP]
simp only [traverse_pure, functor_norm, (· ∘ ·)]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x * y) = Functor.Comp.mk (traverse f <$> traverse g (pure x * y))
[PROOFSTEP]
rw [traverse_mul, ih1, ih2, traverse_mul, Functor.Comp.map_mk]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (Seq.seq (Functor.Comp.mk (((fun x x_1 => x <$> x_1) fun x x_1 => x * x_1) <$> traverse f <$> traverse g (pure x)))
      fun x => Functor.Comp.mk (traverse f <$> traverse g y)) =
    Functor.Comp.mk (traverse f <$> Seq.seq ((fun x x_1 => x * x_1) <$> traverse g (pure x)) fun x => traverse g y)
[PROOFSTEP]
simp only [Function.comp, functor_norm, traverse_mul]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = id.mk (f <$> of x)
ih2 : traverse (pure ∘ f) y = id.mk (f <$> y)
⊢ traverse (pure ∘ f) (of x * y) = id.mk (f <$> (of x * y))
[PROOFSTEP]
rw [traverse_mul, ih1, ih2, map_mul', mul_map_seq]
[GOAL]
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = id.mk (f <$> of x)
ih2 : traverse (pure ∘ f) y = id.mk (f <$> y)
⊢ id.mk (f <$> of x) * id.mk (f <$> y) = id.mk (f <$> of x * f <$> y)
[PROOFSTEP]
rfl
[GOAL]
α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ : FreeSemigroup α
x : α
⊢ (fun {α} => ApplicativeTransformation.app η α) (traverse f (pure x)) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (pure x)
[PROOFSTEP]
simp only [traverse_pure, functor_norm, Function.comp]
[GOAL]
α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
src✝ : LawfulMonad FreeSemigroup := instLawfulMonadFreeSemigroup
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
ih1 :
  (fun {α} => ApplicativeTransformation.app η α) (traverse f (pure x)) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (pure x)
ih2 :
  (fun {α} => ApplicativeTransformation.app η α) (traverse f y) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) y
⊢ (fun {α} => ApplicativeTransformation.app η α) (traverse f (pure x * y)) =
    traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (pure x * y)
[PROOFSTEP]
simp only [traverse_mul, functor_norm, ih1, ih2]
[GOAL]
α : Type u
β : Type v
f : α → β
⊢ MulHom.comp toFreeSemigroup (map f) = MulHom.comp (FreeSemigroup.map f) toFreeSemigroup
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u
β : Type v
f : α → β
⊢ ↑(MulHom.comp toFreeSemigroup (map f)) ∘ of = ↑(MulHom.comp (FreeSemigroup.map f) toFreeSemigroup) ∘ of
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
x✝ x y : FreeMagma α
hx : FreeSemigroup.length (↑toFreeSemigroup x) = length x
hy : FreeSemigroup.length (↑toFreeSemigroup y) = length y
⊢ FreeSemigroup.length (↑toFreeSemigroup (x * y)) = length (x * y)
[PROOFSTEP]
rw [map_mul, FreeSemigroup.length_mul, hx, hy]
[GOAL]
α : Type u
β : Type v
x✝ x y : FreeMagma α
hx : FreeSemigroup.length (↑toFreeSemigroup x) = length x
hy : FreeSemigroup.length (↑toFreeSemigroup y) = length y
⊢ length x + length y = length (x * y)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
⊢ MulHom.comp (↑FreeSemigroup.lift (↑Magma.AssocQuotient.of ∘ FreeMagma.of))
      (↑Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup) =
    MulHom.id (Magma.AssocQuotient (FreeMagma α))
[PROOFSTEP]
ext
[GOAL]
case h.h.h
α : Type u
x✝ : α
⊢ (↑(MulHom.comp
            (MulHom.comp (↑FreeSemigroup.lift (↑Magma.AssocQuotient.of ∘ FreeMagma.of))
              (↑Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup))
            Magma.AssocQuotient.of) ∘
        FreeMagma.of)
      x✝ =
    (↑(MulHom.comp (MulHom.id (Magma.AssocQuotient (FreeMagma α))) Magma.AssocQuotient.of) ∘ FreeMagma.of) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
⊢ MulHom.comp (↑Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup)
      (↑FreeSemigroup.lift (↑Magma.AssocQuotient.of ∘ FreeMagma.of)) =
    MulHom.id (FreeSemigroup α)
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u
⊢ ↑(MulHom.comp (↑Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup)
          (↑FreeSemigroup.lift (↑Magma.AssocQuotient.of ∘ FreeMagma.of))) ∘
      FreeSemigroup.of =
    ↑(MulHom.id (FreeSemigroup α)) ∘ FreeSemigroup.of
[PROOFSTEP]
rfl