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
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)
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)
⊢ Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p
have pure₂ : ∀ (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)),
  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
-- 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)
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)
pure₂ :
  ∀ (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)),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk p <$> (-Pure.pure q))
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (-Pure.pure q) <*> Pure.pure p)
⊢ Prod.mk p <$> y = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p
have pure₃ : ∀ (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),
  Prod.mk p <$> (y₁ + y₂) = (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> (y₁ + y₂) <*> 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
-- 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
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-pure p) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
have neg : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk <$> pure p <*> y)
  ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
Tactic: rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
-- 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
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
neg :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-pure p) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
have neg₁ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
  ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
Tactic: rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
-- 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
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
neg :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
neg₁ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-pure p) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
have neg₂ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
  (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
Tactic: rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
-- 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
ih :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
neg :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
neg₁ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
neg₂ :
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (-(Prod.mk <$> pure p <*> y))
    (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-pure p) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -pure p)
have neg₃ : Eq (α := FreeAbelianGroup (α_1 × β_1)) (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
  (-((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p))
Tactic: rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
y : FreeAbelianGroup β_1
x₁ x₂ : FreeAbelianGroup α_1
ih1 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
ih2 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
have add : HAdd.hAdd (α := FreeAbelianGroup (β_1 → α_1 × β_1)) (Prod.mk <$> x₁) (Prod.mk <$> x₂) <*> y =
  (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
Tactic: rw [FreeAbelianGroup.map_add, add_seq, seq_add, 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
x₁ x₂ : FreeAbelianGroup α_1
ih1 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
ih2 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add :
  HAdd.hAdd (α := FreeAbelianGroup (β_1 → α_1 × β_1)) (Prod.mk <$> x₁) (Prod.mk <$> x₂) <*> y =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
have add₁ : HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
  (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
Tactic: rw [FreeAbelianGroup.map_add, add_seq, seq_add, 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
x₁ x₂ : FreeAbelianGroup α_1
ih1 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
ih2 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add :
  HAdd.hAdd (α := FreeAbelianGroup (β_1 → α_1 × β_1)) (Prod.mk <$> x₁) (Prod.mk <$> x₂) <*> y =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₁ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
have add₂ : HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
Tactic: rw [FreeAbelianGroup.map_add, add_seq, seq_add, 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
x₁ x₂ : FreeAbelianGroup α_1
ih1 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
ih2 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add :
  HAdd.hAdd (α := FreeAbelianGroup (β_1 → α_1 × β_1)) (Prod.mk <$> x₁) (Prod.mk <$> x₂) <*> y =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₁ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₂ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
have add₃ : HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁) (Prod.mk <$> x₂ <*> y) =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
Tactic: rw [FreeAbelianGroup.map_add, add_seq, seq_add, 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
x₁ x₂ : FreeAbelianGroup α_1
ih1 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
ih2 : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add :
  HAdd.hAdd (α := FreeAbelianGroup (β_1 → α_1 × β_1)) (Prod.mk <$> x₁) (Prod.mk <$> x₂) <*> y =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₁ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂
add₂ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) (Prod.mk <$> x₂ <*> y) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
add₃ :
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      (Prod.mk <$> x₂ <*> y) =
    HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
have add₄ : HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂) =
  HAdd.hAdd (α := FreeAbelianGroup (α_1 × β_1)) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)
Tactic: rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
x : FreeAbelianGroup α_1
y : FreeAbelianGroup β_1
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x)
have zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
Tactic: induction x using FreeAbelianGroup.induction_on' with
    | zero => rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
    | pure p =>
      rw [map_pure, pure_seq]
      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]
    | neg p ih => rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
    | add x₁ x₂ ih1 ih2 => rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
x : FreeAbelianGroup α_1
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x)
have pure : ∀ (p : α_1),
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> pure p <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> pure p)
Tactic: induction x using FreeAbelianGroup.induction_on' with
    | zero => rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
    | pure p =>
      rw [map_pure, pure_seq]
      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]
    | neg p ih => rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
    | add x₁ x₂ ih1 ih2 => rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
x : FreeAbelianGroup α_1
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
pure :
  ∀ (p : α_1),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x)
have neg : ∀ (p : α_1)
  (ih :
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)),
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-Pure.pure p) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -Pure.pure p)
Tactic: induction x using FreeAbelianGroup.induction_on' with
    | zero => rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
    | pure p =>
      rw [map_pure, pure_seq]
      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]
    | neg p ih => rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
    | add x₁ x₂ ih1 ih2 => rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
x : FreeAbelianGroup α_1
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
pure :
  ∀ (p : α_1),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)
neg :
  ∀ (p : α_1)
    (ih :
      Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-Pure.pure p) <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -Pure.pure p)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x)
have add : ∀ (x₁ x₂ : FreeAbelianGroup α_1)
  (ih1 :
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁))
  (ih2 :
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)),
  Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
    ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
Tactic: induction x using FreeAbelianGroup.induction_on' with
    | zero => rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
    | pure p =>
      rw [map_pure, pure_seq]
      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]
    | neg p ih => rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
    | add x₁ x₂ ih1 ih2 => rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        x :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x : FreeAbelianGroup β) :
      γ)
have zero : Eq.{u_4 + 1} (α := γ)
  ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
        (a : FreeAbelianGroup α) → γ)
      0 :
    γ)
  ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
        (a : FreeAbelianGroup β) → γ)
      ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) 0) :
    γ)
Tactic: induction x using FreeAbelianGroup.induction_on with
  | zero => simp only [map_zero]
  | of => simp only [lift_apply_of, map, Function.comp]
  | neg _ h => simp only [h, map_neg]
  | add _ _ h₁ h₂ => simp only [h₁, h₂, map_add]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
zero :
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        0 :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) 0) :
      γ)
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        x :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x : FreeAbelianGroup β) :
      γ)
have of : ∀ (x : α),
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (of x) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (of x) : FreeAbelianGroup β) :
      γ)
Tactic: induction x using FreeAbelianGroup.induction_on with
  | zero => simp only [map_zero]
  | of => simp only [lift_apply_of, map, Function.comp]
  | neg _ h => simp only [h, map_neg]
  | add _ _ h₁ h₂ => simp only [h₁, h₂, map_add]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
zero :
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        0 :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) 0) :
      γ)
of :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := γ)
      ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
            (a : FreeAbelianGroup α) → γ)
          (FreeAbelianGroup.of x) :
        γ)
      ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
            (a : FreeAbelianGroup β) → γ)
          ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (FreeAbelianGroup.of x) : FreeAbelianGroup β) :
        γ)
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        x :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x : FreeAbelianGroup β) :
      γ)
have neg : ∀ (x : α)
  (h :
    Eq.{u_4 + 1} (α := γ)
      ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
            (a : FreeAbelianGroup α) → γ)
          (FreeAbelianGroup.of x) :
        γ)
      ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
            (a : FreeAbelianGroup β) → γ)
          ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (FreeAbelianGroup.of x) : FreeAbelianGroup β) :
        γ)),
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (-FreeAbelianGroup.of x) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (-FreeAbelianGroup.of x) : FreeAbelianGroup β) :
      γ)
Tactic: induction x using FreeAbelianGroup.induction_on with
  | zero => simp only [map_zero]
  | of => simp only [lift_apply_of, map, Function.comp]
  | neg _ h => simp only [h, map_neg]
  | add _ _ h₁ h₂ => simp only [h₁, h₂, map_add]
Cleared hypotheses: x