awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma α_1)) (traverse pure x) (pure x)
ih2 : Eq (α := Id (FreeMagma α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> traverse pure x <*> traverse pure y)
    (pure (x * y))
rw₁ :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> traverse pure y) (pure (x * y))
rw₂ : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> pure y) (pure (x * y))
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))
have rw₃ : Eq (α := Id (FreeMagma α_1))
  ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> (fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x)
  (pure (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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma α_1)) (traverse pure x) (pure x)
ih2 : Eq (α := Id (FreeMagma α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> traverse pure x <*> traverse pure y)
    (pure (x * y))
rw₁ :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> traverse pure y) (pure (x * y))
rw₂ : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> pure y) (pure (x * y))
rw₃ :
  Eq (α := Id (FreeMagma α_1))
    ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> (fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x)
    (pure (x * y))
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))
have rw₄ : Eq (α := Id (FreeMagma α_1))
  ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> pure fun (x2 : FreeMagma α_1) ↦ x * x2) (pure (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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma α_1)) (traverse pure x) (pure x)
ih2 : Eq (α := Id (FreeMagma α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> traverse pure x <*> traverse pure y)
    (pure (x * y))
rw₁ :
  Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> traverse pure y) (pure (x * y))
rw₂ : Eq (α := Id (FreeMagma α_1)) ((fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x <*> pure y) (pure (x * y))
rw₃ :
  Eq (α := Id (FreeMagma α_1))
    ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> (fun (x1 x2 : FreeMagma α_1) ↦ x1 * x2) <$> pure x)
    (pure (x * y))
rw₄ :
  Eq (α := Id (FreeMagma α_1))
    ((fun (h : FreeMagma α_1 → FreeMagma α_1) ↦ h y) <$> pure fun (x2 : FreeMagma α_1) ↦ x * x2) (pure (x * y))
⊢ Eq (α := Id (FreeMagma α_1)) (traverse pure (x * y)) (pure (x * y))
have rw₅ : Eq (α := Id (FreeMagma α_1)) (pure ((fun (x2 : FreeMagma α_1) ↦ x * x2) y)) (pure (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 x y : FreeMagma α_1
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))
have rw : Eq (α := Functor.Comp G F_1 (FreeMagma γ))
  ((fun (x1 x2 : FreeMagma γ) ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
    Functor.Comp.mk (traverse f <$> traverse g y))
  (Functor.Comp.mk (traverse f <$> ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse g x <*> traverse g y)))
Tactic: rw [traverse_mul, ih1, ih2, traverse_mul]
-- 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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw : Eq (α := Id (FreeMagma β_1))
  ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw₁ : Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
  (pure (f <$> (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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
rw₁ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (x * y)))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw₂ : Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
  (pure (f <$> (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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
rw₁ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (x * y)))
rw₂ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> (x * y)))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw₃ : Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
  (pure (f <$> 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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
rw₁ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (x * y)))
rw₂ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> (x * y)))
rw₃ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw₄ : Eq (α := Id (FreeMagma β_1)) ((pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2) <*> pure (f <$> y))
  (pure (f <$> 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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
rw₁ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (x * y)))
rw₂ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> (x * y)))
rw₃ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
rw₄ :
  Eq (α := Id (FreeMagma β_1)) ((pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw₅ : Eq (α := Id (FreeMagma β_1))
  ((fun (h : FreeMagma β_1 → FreeMagma β_1) ↦ h (f <$> y)) <$> pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2)
  (pure (f <$> 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 x y : FreeMagma α_1
ih1 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) x) (pure (f <$> x))
ih2 : Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeMagma β_1))
    ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) x <*> traverse (pure ∘ f) y) (pure (f <$> (x * y)))
rw₁ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (x * y)))
rw₂ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> (x * y)))
rw₃ :
  Eq (α := Id (FreeMagma β_1)) ((fun (x1 x2 : FreeMagma β_1) ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
rw₄ :
  Eq (α := Id (FreeMagma β_1)) ((pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2) <*> pure (f <$> y))
    (pure (f <$> x * f <$> y))
rw₅ :
  Eq (α := Id (FreeMagma β_1))
    ((fun (h : FreeMagma β_1 → FreeMagma β_1) ↦ h (f <$> y)) <$> pure fun (x2 : FreeMagma β_1) ↦ f <$> x * x2)
    (pure (f <$> x * f <$> y))
⊢ Eq (α := Id (FreeMagma β_1)) (traverse (pure ∘ f) (x * y)) (pure (f <$> (x * y)))
have rw₆ : Eq (α := Id (FreeMagma β_1)) (pure ((fun (x2 : FreeMagma β_1) ↦ f <$> x * x2) (f <$> y))) (pure (f <$> 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
inst : Mul α
x y : AssocQuotient α
⊢ AssocQuotient α
have refine_1 : ∀ (a b₁ b₂ : α),
  AssocRel α b₁ b₂ →
    Eq.{u + 1} (α := AssocQuotient α) ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a b₁)
      ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a b₂)
Tactic: refine Quot.liftOn₂ x y (fun x y ↦ Quot.mk _ (x * y)) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
refine_1 :
  ∀ (a b₁ b₂ : α),
    AssocRel α b₁ b₂ →
      Eq.{u + 1} (α := AssocQuotient α) ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a b₁)
        ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a b₂)
⊢ AssocQuotient α
have refine_2 : ∀ (a₁ a₂ b : α),
  AssocRel α a₁ a₂ →
    Eq.{u + 1} (α := AssocQuotient α) ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a₁ b)
      ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a₂ b)
Tactic: refine Quot.liftOn₂ x y (fun x y ↦ Quot.mk _ (x * y)) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : 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))))
have refine_1 : Quot.mk (AssocRel α) (a * c * (d * e * f)) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
Tactic: rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
a c d e f : α
refine_1 : Quot.mk (AssocRel α) (a * c * (d * e * f)) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
⊢ Quot.mk (AssocRel α) (a * (c * (d * e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
have refine_1₁ : Quot.mk (AssocRel α) (a * c * (d * (e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
Tactic: rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
a c d e f : α
refine_1 : Quot.mk (AssocRel α) (a * c * (d * e * f)) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
refine_1₁ : Quot.mk (AssocRel α) (a * c * (d * (e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
⊢ Quot.mk (AssocRel α) (a * (c * (d * e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
have refine_1₂ : Quot.mk (AssocRel α) (a * (c * (d * (e * f)))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
Tactic: rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : 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)
have refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₃ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₃ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₄ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₃ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₄ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₅ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₃ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₄ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
refine_2₅ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₆ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * f * b))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₃ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₄ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
refine_2₅ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
refine_2₆ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * f * b))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
have refine_2₇ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * (f * b)))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ (((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
      (of x * y) =
    HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β)
have rw : HMul.hMul (α := β) (β := β)
    ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
        (of x) :
      β)
    ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
        y :
      β) =
  HMul.hMul (β := β) (f x)
    ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
        y :
      β)
Tactic: rw [map_mul, lift_of]
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
rw :
  HMul.hMul (α := β) (β := β)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          (of x) :
        β)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β) =
    HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β)
⊢ (((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
      (of x * y) =
    HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β)
have rw₁ : HMul.hMul (β := β) (f x)
    ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
        y :
      β) =
  HMul.hMul (β := β) (f x)
    ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
        y :
      β)
Tactic: rw [map_mul, lift_of]
-- 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
⊢ id <$> (pure x * y) = pure x * y
have rw : id <$> pure x * id <$> y = pure x * y
Tactic: rw [map_mul', ih1, ih2]
-- 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
⊢ id <$> (pure x * y) = pure x * y
have rw₁ : pure x * id <$> y = pure x * y
Tactic: rw [map_mul', ih1, ih2]