awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
⊢ f x >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
have rw : f x >>= g = f x >>= g
Tactic: rw [pure_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
⊢ pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
have iterate : f x >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
Tactic: iterate 2 rw [pure_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
have rw : -(pure x >>= f) >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [neg_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
have rw : -(pure x >>= f >>= g) = -pure x >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [neg_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun (x : α_1) ↦ f x >>= g
have rw : Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-pure x >>= fun (x : α_1) ↦ f x >>= g)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun (x : α_1) ↦ f x >>= g
have try : Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-pure x >>= fun (x : α_1) ↦ f x >>= g)
Tactic: try rw [ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-pure x >>= fun (x : α_1) ↦ f x >>= g)
have rw : Eq (α := FreeAbelianGroup γ) (-(pure x >>= fun (x : α_1) ↦ f x >>= g)) (-(pure x >>= fun (x : α_1) ↦ f x >>= g))
Tactic: rw [neg_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x : α_1
ih : pure x >>= f >>= g = pure x >>= fun (x : α_1) ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
have iterate : -(pure x >>= f) >>= g = -pure x >>= fun (x : α_1) ↦ f x >>= g
Tactic: iterate 3 rw [neg_bind] <;> try rw [ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
have rw : (x >>= f) + (y >>= f) >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [add_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
have rw : (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [add_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun (x : α_1) ↦ f x >>= g
have rw : HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
  x + y >>= fun (x : α_1) ↦ f x >>= g
Tactic: rw [ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun (x : α_1) ↦ f x >>= g
have try : HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
  x + y >>= fun (x : α_1) ↦ f x >>= g
Tactic: try rw [ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
    x + y >>= fun (x : α_1) ↦ f x >>= g
have rw : HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g) =
  HAdd.hAdd (α := FreeAbelianGroup γ) (x >>= fun (x : α_1) ↦ f x >>= g) (y >>= fun (x : α_1) ↦ f x >>= g)
Tactic: rw [add_bind]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 γ : Type u
x_1 : FreeAbelianGroup α_1
f : α_1 → FreeAbelianGroup β_1
g : β_1 → FreeAbelianGroup γ
x y : FreeAbelianGroup α_1
ihx : x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
have iterate : (x >>= f) + (y >>= f) >>= g = x + y >>= fun (x : α_1) ↦ f x >>= g
Tactic: iterate 3 rw [add_bind] <;> try rw [ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
have zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
Tactic: rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
have zero₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
Tactic: rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
zero₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
have zero₂ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 0
Tactic: rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
p : α_1
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
have pure : Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p
Tactic: rw [map_pure, pure_seq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> pure p)
have pure : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> pure p)
Tactic: rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
pure : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
have pure₁ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 (0 <*> Pure.pure p)
Tactic: rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
pure : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
pure₁ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 (0 <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
have pure₂ : Eq.{u + 1} (α := FreeAbelianGroup (α_1 × β_1)) 0 0
Tactic: rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> pure q <*> pure p)
have pure : Eq (α := FreeAbelianGroup (α_1 × β_1)) (pure (p, q)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> pure q <*> pure p)
Tactic: rw [map_pure, map_pure, pure_seq, map_pure]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
have pure₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((Pure.pure fun (a : α_1) ↦ (a, q)) <*> Pure.pure p)
Tactic: rw [map_pure, map_pure, pure_seq, map_pure]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((Pure.pure fun (a : α_1) ↦ (a, q)) <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
have pure₂ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((fun (a : α_1) ↦ (a, q)) <$> Pure.pure p)
Tactic: rw [map_pure, map_pure, pure_seq, map_pure]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((Pure.pure fun (a : α_1) ↦ (a, q)) <*> Pure.pure p)
pure₂ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) ((fun (a : α_1) ↦ (a, q)) <$> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
have pure₃ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Pure.pure (p, q)) (Pure.pure (p, q))
Tactic: rw [map_pure, map_pure, pure_seq, map_pure]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> pure q <*> pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-pure q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-pure q) <*> pure p)
have pure : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> pure q)
  ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-pure q) <*> pure p)
Tactic: rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-Pure.pure q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
have pure₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
  (-(fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
Tactic: rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
pure₁ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    (-(fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-Pure.pure q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
have pure₂ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
  (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
Tactic: rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
q : β_1
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
pure₁ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    (-(fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
pure₂ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk p <$> Pure.pure q)
    (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-Pure.pure q))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
have pure₃ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
  (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p))
Tactic: rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
y₁ y₂ : FreeAbelianGroup β_1
ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> pure p
have pure : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> pure p
Tactic: rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
y₁ y₂ : FreeAbelianGroup β_1
ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p
ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p
pure : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
⊢ Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
have pure₁ : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 → α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂) <*>
    Pure.pure p
Tactic: rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
y₁ y₂ : FreeAbelianGroup β_1
ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p
ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p
pure : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
pure₁ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 → α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂) <*>
      Pure.pure p
⊢ Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
have pure₂ : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
Tactic: rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
y₁ y₂ : FreeAbelianGroup β_1
ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p
ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p
pure : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
pure₁ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 → α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂) <*>
      Pure.pure p
pure₂ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
⊢ Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
have pure₃ : ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p) + Prod.mk p <$> y₂ =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
Tactic: rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
p : α_1
y₁ y₂ : FreeAbelianGroup β_1
ih1 : Prod.mk p <$> y₁ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p
ih2 : Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p
pure : Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
pure₁ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 → α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂) <*>
      Pure.pure p
pure₂ :
  Prod.mk p <$> y₁ + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
pure₃ :
  ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p) + Prod.mk p <$> y₂ =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
⊢ Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> Pure.pure p
have pure₄ : HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p) =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₁ <*> Pure.pure p)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y₂ <*> Pure.pure p)
Tactic: rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
p : α_1
⊢ Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p
have pure : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> pure p)
Tactic: induction y using FreeAbelianGroup.induction_on' with
      | zero => rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
      | pure q => rw [map_pure, map_pure, pure_seq, map_pure]
      | neg q ih => rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
      | add y₁ y₂ ih1 ih2 =>
        rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
p : α_1
pure :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> 0) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> 0 <*> Pure.pure p)
⊢ Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p
have pure₁ : ∀ (q : β_1),
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> Pure.pure q)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> Pure.pure q <*> Pure.pure p)
Tactic: induction y using FreeAbelianGroup.induction_on' with
      | zero => rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
      | pure q => rw [map_pure, map_pure, pure_seq, map_pure]
      | neg q ih => rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
      | add y₁ y₂ ih1 ih2 =>
        rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
Cleared hypotheses: y