awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := FreeSemigroup α_1) (id <$> pure x) (pure x)
ih2 : id <$> y = y
rw : id <$> pure x * id <$> y = pure x * y
rw₁ : pure x * id <$> y = pure x * y
⊢ id <$> (pure x * y) = pure x * y
have rw₂ : pure x * y = pure x * y
Tactic: rw [map_mul', ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeSemigroup α_1
g : α_1 → FreeSemigroup β_1
f : β_1 → FreeSemigroup γ
x : α_1
y : FreeSemigroup α_1
ih1 : pure x >>= g >>= f = pure x >>= fun (x : α_1) ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun (x : α_1) ↦ g x >>= f
⊢ pure x * y >>= g >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
have rw : (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeSemigroup α_1
g : α_1 → FreeSemigroup β_1
f : β_1 → FreeSemigroup γ
x : α_1
y : FreeSemigroup α_1
ih1 : pure x >>= g >>= f = pure x >>= fun (x : α_1) ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun (x : α_1) ↦ g x >>= f
rw : (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
⊢ pure x * y >>= g >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
have rw₁ : (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun (x : α_1) ↦ g x >>= f
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeSemigroup α_1
g : α_1 → FreeSemigroup β_1
f : β_1 → FreeSemigroup γ
x : α_1
y : FreeSemigroup α_1
ih1 : pure x >>= g >>= f = pure x >>= fun (x : α_1) ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun (x : α_1) ↦ g x >>= f
rw : (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₁ : (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun (x : α_1) ↦ g x >>= f
⊢ pure x * y >>= g >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
have rw₂ : (pure x >>= g >>= f) * (y >>= g >>= f) =
  HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeSemigroup α_1
g : α_1 → FreeSemigroup β_1
f : β_1 → FreeSemigroup γ
x : α_1
y : FreeSemigroup α_1
ih1 : pure x >>= g >>= f = pure x >>= fun (x : α_1) ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun (x : α_1) ↦ g x >>= f
rw : (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₁ : (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₂ :
  (pure x >>= g >>= f) * (y >>= g >>= f) =
    HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
⊢ pure x * y >>= g >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
have rw₃ : (pure x >>= fun (x : α_1) ↦ g x >>= f) * (y >>= g >>= f) =
  HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeSemigroup α_1
g : α_1 → FreeSemigroup β_1
f : β_1 → FreeSemigroup γ
x : α_1
y : FreeSemigroup α_1
ih1 : pure x >>= g >>= f = pure x >>= fun (x : α_1) ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun (x : α_1) ↦ g x >>= f
rw : (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₁ : (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₂ :
  (pure x >>= g >>= f) * (y >>= g >>= f) =
    HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
rw₃ :
  (pure x >>= fun (x : α_1) ↦ g x >>= f) * (y >>= g >>= f) =
    HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
⊢ pure x * y >>= g >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
have rw₄ : HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f) =
  HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
Tactic: rw [mul_bind, mul_bind, mul_bind, ih1, ih2]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
inst_1 : LawfulApplicative m
x_1 y_1 : FreeSemigroup α
x_2 : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl : FreeSemigroup α } * { head := y, tail := L2 : FreeSemigroup α }) =
      (fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F { head := x, tail := tl : FreeSemigroup α } <*>
        traverse F { head := y, tail := L2 }
x : α
⊢ Eq (α := m (FreeSemigroup β))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*>
      traverse F ({ head := hd, tail := tl : FreeSemigroup α } * { head := y, tail := L2 : FreeSemigroup α }))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$>
        ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 })
have rw : Eq (α := m (FreeSemigroup β))
  ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*>
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F { head := hd, tail := tl : FreeSemigroup α } <*>
      traverse F { head := y, tail := L2 }))
  ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$>
      ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
    traverse F { head := y, tail := L2 })
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))
have rw : Eq (α := Id (FreeSemigroup α_1))
  ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))
have rw₁ : Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> traverse pure y)
  (pure (of x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
rw₁ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> traverse pure y)
    (pure (of x * y))
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))
have rw₂ : Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> pure y)
  (pure (of x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
rw₁ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> traverse pure y)
    (pure (of x * y))
rw₂ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> pure y)
    (pure (of x * y))
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))
have rw₃ : Eq (α := Id (FreeSemigroup α_1))
  ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$>
    (fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x))
  (pure (of x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
rw₁ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> traverse pure y)
    (pure (of x * y))
rw₂ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> pure y)
    (pure (of x * y))
rw₃ :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$>
      (fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x))
    (pure (of x * y))
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))
have rw₄ : Eq (α := Id (FreeSemigroup α_1))
  ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$> pure fun (x2 : FreeSemigroup α_1) ↦ of x * x2)
  (pure (of x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
rw₁ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> traverse pure y)
    (pure (of x * y))
rw₂ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> pure y)
    (pure (of x * y))
rw₃ :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$>
      (fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x))
    (pure (of x * y))
rw₄ :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$> pure fun (x2 : FreeSemigroup α_1) ↦ of x * x2)
    (pure (of x * y))
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))
have rw₅ : Eq (α := Id (FreeSemigroup α_1)) (pure ((fun (x2 : FreeSemigroup α_1) ↦ of x * x2) y)) (pure (of x * y))
Tactic: rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 :
  Eq (α := Functor.Comp G F_1 (FreeSemigroup γ)) (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))
have rw : Eq (α := Functor.Comp G F_1 (FreeSemigroup γ))
  (Functor.Comp.mk
      ((fun (x : F_1 (FreeSemigroup γ)) ↦ (fun (x1 x2 : FreeSemigroup γ) ↦ x1 * x2) <$> x) <$>
        traverse f <$> traverse g (pure x)) <*>
    Functor.Comp.mk (traverse f <$> traverse g y))
  (Functor.Comp.mk
    (traverse f <$> ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y)))
Tactic: rw [traverse_mul, ih1, ih2, traverse_mul, Functor.Comp.map_mk]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw : Eq (α := Id (FreeSemigroup β_1))
  ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
  (pure (f <$> (of x * y)))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw₁ : Eq (α := Id (FreeSemigroup β_1))
  ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
  (pure (f <$> (of x * y)))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₁ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw₂ : Eq (α := Id (FreeSemigroup β_1)) ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y))
  (pure (f <$> (of x * y)))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₁ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₂ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> (of x * y)))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw₃ : Eq (α := Id (FreeSemigroup β_1)) ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y))
  (pure (f <$> of x * f <$> y))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₁ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₂ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> (of x * y)))
rw₃ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> of x * f <$> y))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw₄ : Eq (α := Id (FreeSemigroup β_1)) ((pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2) <*> pure (f <$> y))
  (pure (f <$> of x * f <$> y))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₁ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₂ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> (of x * y)))
rw₃ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> of x * f <$> y))
rw₄ :
  Eq (α := Id (FreeSemigroup β_1)) ((pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2) <*> pure (f <$> y))
    (pure (f <$> of x * f <$> y))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw₅ : Eq (α := Id (FreeSemigroup β_1))
  ((fun (h : FreeSemigroup β_1 → FreeSemigroup β_1) ↦ h (f <$> y)) <$>
    pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2)
  (pure (f <$> of x * f <$> y))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₁ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₂ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> (of x * y)))
rw₃ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> of x * f <$> y))
rw₄ :
  Eq (α := Id (FreeSemigroup β_1)) ((pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2) <*> pure (f <$> y))
    (pure (f <$> of x * f <$> y))
rw₅ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (h : FreeSemigroup β_1 → FreeSemigroup β_1) ↦ h (f <$> y)) <$>
      pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2)
    (pure (f <$> of x * f <$> y))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))
have rw₆ : Eq (α := Id (FreeSemigroup β_1)) (pure ((fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2) (f <$> y)))
  (pure (f <$> of x * f <$> y))
Tactic: rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ MulHom.comp toFreeSemigroup (map f) = (FreeSemigroup.map f).comp toFreeSemigroup
have h : Eq (α := α → FreeSemigroup β) ((⇑(MulHom.comp toFreeSemigroup (map f)) : (a : FreeMagma α) → FreeSemigroup β) ∘ of)
  ((⇑((FreeSemigroup.map f).comp toFreeSemigroup) : (a : FreeMagma α) → FreeSemigroup β) ∘ of)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
x_1 x y : FreeMagma α
hx : FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) x) = x.length
hy : FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) y) = y.length
⊢ FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) (x * y)) = (x * y).length
have rw : x.length + y.length = (x * y).length
Tactic: rw [map_mul, FreeSemigroup.length_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Magma.AssocQuotient (FreeMagma α) →ₙ* Magma.AssocQuotient (FreeMagma α))
    (MulHom.comp (N := FreeSemigroup α)
      ((FreeSemigroup.lift :
          (a : α → Magma.AssocQuotient (FreeMagma α)) → FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
        ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of))
      ((Magma.AssocQuotient.lift :
          (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
        FreeMagma.toFreeSemigroup))
    (MulHom.id (Magma.AssocQuotient (FreeMagma α)))
have h : ∀ (x : α),
  Eq (α := Magma.AssocQuotient (FreeMagma α))
    (((⇑(MulHom.comp
              (MulHom.comp (N := FreeSemigroup α)
                ((FreeSemigroup.lift :
                    (a : α → Magma.AssocQuotient (FreeMagma α)) → FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
                  ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of))
                ((Magma.AssocQuotient.lift :
                    (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
                  FreeMagma.toFreeSemigroup))
              Magma.AssocQuotient.of) :
          (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘
        FreeMagma.of)
      x)
    (((⇑(MulHom.comp (MulHom.id (Magma.AssocQuotient (FreeMagma α))) Magma.AssocQuotient.of) :
          (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘
        FreeMagma.of)
      x)
Tactic: ext