awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3)
ih₂ : x * y₂ * FreeAbelianGroup.of L3 = x * (y₂ * FreeAbelianGroup.of L3)
of : x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3 + y₂ * FreeAbelianGroup.of L3)
of₁ : (x * y₁ + x * y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3 + y₂ * FreeAbelianGroup.of L3)
of₂ : (x * y₁ + x * y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
of₃ :
  x * y₁ * FreeAbelianGroup.of L3 + x * y₂ * FreeAbelianGroup.of L3 =
    x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
of₄ :
  x * (y₁ * FreeAbelianGroup.of L3) + x * y₂ * FreeAbelianGroup.of L3 =
    x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
⊢ x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
have of₅ : x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3) =
  x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
Tactic: rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
⊢ x * y * of L3 = x * (y * of L3)
have of : x * 0 * of L3 = x * (0 * of L3)
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
of : x * 0 * FreeAbelianGroup.of L3 = x * (0 * FreeAbelianGroup.of L3)
⊢ x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)
have of₁ : ∀ (L2 : α), x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
of : x * 0 * FreeAbelianGroup.of L3 = x * (0 * FreeAbelianGroup.of L3)
of₁ :
  ∀ (L2 : α),
    x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
⊢ x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)
have of₂ : ∀ (L2 : α)
  (ih : x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)),
  x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
of : x * 0 * FreeAbelianGroup.of L3 = x * (0 * FreeAbelianGroup.of L3)
of₁ :
  ∀ (L2 : α),
    x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₂ :
  ∀ (L2 : α)
    (ih : x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)),
    x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
⊢ x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)
have of₃ : ∀ (y₁ y₂ : FreeAbelianGroup α) (ih₁ : x * y₁ * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3))
  (ih₂ : x * y₂ * FreeAbelianGroup.of L3 = x * (y₂ * FreeAbelianGroup.of L3)),
  x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ x * y * -of L3 = x * (y * -of L3)
have neg : -(x * y * of L3) = x * (y * -of L3)
Tactic: rw [mul_neg, mul_neg, mul_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
neg : -(x * y * of L3) = x * (y * -of L3)
⊢ x * y * -of L3 = x * (y * -of L3)
have neg₁ : -(x * y * of L3) = x * -(y * of L3)
Tactic: rw [mul_neg, mul_neg, mul_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
neg : -(x * y * of L3) = x * (y * -of L3)
neg₁ : -(x * y * of L3) = x * -(y * of L3)
⊢ x * y * -of L3 = x * (y * -of L3)
have neg₂ : -(x * y * of L3) = -(x * (y * of L3))
Tactic: rw [mul_neg, mul_neg, mul_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
neg : -(x * y * of L3) = x * (y * -of L3)
neg₁ : -(x * y * of L3) = x * -(y * of L3)
neg₂ : -(x * y * of L3) = -(x * (y * of L3))
⊢ x * y * -of L3 = x * (y * -of L3)
have neg₃ : -(x * (y * of L3)) = -(x * (y * of L3))
Tactic: rw [mul_neg, mul_neg, mul_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
have add : x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
Tactic: rw [mul_add, mul_add, mul_add, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
add : x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
have add₁ : x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)
Tactic: rw [mul_add, mul_add, mul_add, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
add : x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
add₁ : x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
have add₂ : x * y * z₁ + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
Tactic: rw [mul_add, mul_add, mul_add, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
add : x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
add₁ : x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)
add₂ : x * y * z₁ + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
have add₃ : x * (y * z₁) + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
Tactic: rw [mul_add, mul_add, mul_add, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
add : x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
add₁ : x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)
add₂ : x * y * z₁ + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
add₃ : x * (y * z₁) + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
have add₄ : x * (y * z₁) + x * (y * z₂) = x * (y * z₁) + x * (y * z₂)
Tactic: rw [mul_add, mul_add, mul_add, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z : FreeAbelianGroup α
⊢ x * y * z = x * (y * z)
have zero : x * y * 0 = x * (y * 0)
Tactic: induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z : FreeAbelianGroup α
zero : x * y * 0 = x * (y * 0)
⊢ x * y * z = x * (y * z)
have of : ∀ (L3 : α), x * y * of L3 = x * (y * of L3)
Tactic: induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z : FreeAbelianGroup α
zero : x * y * 0 = x * (y * 0)
of : ∀ (L3 : α), x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)
⊢ x * y * z = x * (y * z)
have neg : ∀ (L3 : α) (ih : x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)),
  x * y * -FreeAbelianGroup.of L3 = x * (y * -FreeAbelianGroup.of L3)
Tactic: induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z : FreeAbelianGroup α
zero : x * y * 0 = x * (y * 0)
of : ∀ (L3 : α), x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)
neg :
  ∀ (L3 : α) (ih : x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)),
    x * y * -FreeAbelianGroup.of L3 = x * (y * -FreeAbelianGroup.of L3)
⊢ x * y * z = x * (y * z)
have add : ∀ (z₁ z₂ : FreeAbelianGroup α) (ih₁ : x * y * z₁ = x * (y * z₁)) (ih₂ : x * y * z₂ = x * (y * z₂)),
  x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
Tactic: induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x : FreeAbelianGroup α
⊢ 1 * x = x
have simp_rw : ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    x =
  x
Tactic: simp_rw [mul_def, one_def, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
have of : of (1 * L) = of L
Tactic: rw [lift_apply_of, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
of : FreeAbelianGroup.of (1 * L) = FreeAbelianGroup.of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          FreeAbelianGroup.of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of L) =
    FreeAbelianGroup.of L
have of₁ : FreeAbelianGroup.of L = FreeAbelianGroup.of L
Tactic: rw [lift_apply_of, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
ih :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (-of L) =
    -of L
have neg : -((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
  -of L
Tactic: rw [map_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
ih :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
neg :
  -((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of L) =
    -of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (-of L) =
    -of L
have neg₁ : -of L = -of L
Tactic: rw [map_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x1 x2 : FreeAbelianGroup α
ih1 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x1 =
    x1
ih2 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x2 =
    x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2
have add : HAdd.hAdd (α := FreeAbelianGroup α) (β := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        x1 :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        x2 :
      FreeAbelianGroup α) =
  x1 + x2
Tactic: rw [map_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x1 x2 : FreeAbelianGroup α
ih1 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x1 =
    x1
ih2 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x2 =
    x2
add :
  HAdd.hAdd (α := FreeAbelianGroup α) (β := FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x1 :
        FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2
have add₁ : HAdd.hAdd (β := FreeAbelianGroup α) x1
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        x2 :
      FreeAbelianGroup α) =
  x1 + x2
Tactic: rw [map_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x1 x2 : FreeAbelianGroup α
ih1 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x1 =
    x1
ih2 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x2 =
    x2
add :
  HAdd.hAdd (α := FreeAbelianGroup α) (β := FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x1 :
        FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
add₁ :
  HAdd.hAdd (β := FreeAbelianGroup α) x1
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2
have add₂ : x1 + x2 = x1 + x2
Tactic: rw [map_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x : FreeAbelianGroup α
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have zero : Eq.{u + 1} (α := FreeAbelianGroup α)
  (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    0)
  0
Tactic: induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, one_mul]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]
Cleared hypotheses: x