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 : CommMonoid α
s t : α
ih : FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s
of : -(FreeAbelianGroup.of s * FreeAbelianGroup.of t) = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
of₁ : -(FreeAbelianGroup.of t * FreeAbelianGroup.of s) = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * -FreeAbelianGroup.of t = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
have of₂ : -FreeAbelianGroup.of t * FreeAbelianGroup.of s = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
Tactic: rw [mul_neg, ih, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ of s * (y1 + y2) = (y1 + y2) * of s
have of : of s * y1 + of s * y2 = (y1 + y2) * of s
Tactic: rw [mul_add, add_mul, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : FreeAbelianGroup.of s * y1 = y1 * FreeAbelianGroup.of s
ih2 : FreeAbelianGroup.of s * y2 = y2 * FreeAbelianGroup.of s
of : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = (y1 + y2) * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * (y1 + y2) = (y1 + y2) * FreeAbelianGroup.of s
have of₁ : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
Tactic: rw [mul_add, add_mul, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : FreeAbelianGroup.of s * y1 = y1 * FreeAbelianGroup.of s
ih2 : FreeAbelianGroup.of s * y2 = y2 * FreeAbelianGroup.of s
of : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = (y1 + y2) * FreeAbelianGroup.of s
of₁ : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * (y1 + y2) = (y1 + y2) * FreeAbelianGroup.of s
have of₂ : y1 * FreeAbelianGroup.of s + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
Tactic: rw [mul_add, add_mul, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : FreeAbelianGroup.of s * y1 = y1 * FreeAbelianGroup.of s
ih2 : FreeAbelianGroup.of s * y2 = y2 * FreeAbelianGroup.of s
of : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = (y1 + y2) * FreeAbelianGroup.of s
of₁ : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
of₂ : y1 * FreeAbelianGroup.of s + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * (y1 + y2) = (y1 + y2) * FreeAbelianGroup.of s
have of₃ : y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
Tactic: rw [mul_add, add_mul, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
⊢ of s * y = y * of s
have of : of s * 0 = 0 * of s
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
of : FreeAbelianGroup.of s * 0 = 0 * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s
have of₁ : ∀ (t : α), FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
of : FreeAbelianGroup.of s * 0 = 0 * FreeAbelianGroup.of s
of₁ : ∀ (t : α), FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s
have of₂ : ∀ (t : α) (ih : FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s),
  FreeAbelianGroup.of s * -FreeAbelianGroup.of t = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
of : FreeAbelianGroup.of s * 0 = 0 * FreeAbelianGroup.of s
of₁ : ∀ (t : α), FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s
of₂ :
  ∀ (t : α) (ih : FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s),
    FreeAbelianGroup.of s * -FreeAbelianGroup.of t = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s
have of₃ : ∀ (y1 y2 : FreeAbelianGroup α) (ih1 : FreeAbelianGroup.of s * y1 = y1 * FreeAbelianGroup.of s)
  (ih2 : FreeAbelianGroup.of s * y2 = y2 * FreeAbelianGroup.of s),
  FreeAbelianGroup.of s * (y1 + y2) = (y1 + y2) * FreeAbelianGroup.of s
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
⊢ -of s * y = y * -of s
have neg : -(of s * y) = y * -of s
Tactic: rw [neg_mul, ih, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
neg : -(of s * y) = y * -of s
⊢ -of s * y = y * -of s
have neg₁ : -(y * of s) = y * -of s
Tactic: rw [neg_mul, ih, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
neg : -(of s * y) = y * -of s
neg₁ : -(y * of s) = y * -of s
⊢ -of s * y = y * -of s
have neg₂ : y * -of s = y * -of s
Tactic: rw [neg_mul, ih, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)
have add : x1 * y + x2 * y = y * (x1 + x2)
Tactic: rw [add_mul, mul_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
add : x1 * y + x2 * y = y * (x1 + x2)
⊢ (x1 + x2) * y = y * (x1 + x2)
have add₁ : x1 * y + x2 * y = y * x1 + y * x2
Tactic: rw [add_mul, mul_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
add : x1 * y + x2 * y = y * (x1 + x2)
add₁ : x1 * y + x2 * y = y * x1 + y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)
have add₂ : y * x1 + x2 * y = y * x1 + y * x2
Tactic: rw [add_mul, mul_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
add : x1 * y + x2 * y = y * (x1 + x2)
add₁ : x1 * y + x2 * y = y * x1 + y * x2
add₂ : y * x1 + x2 * y = y * x1 + y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)
have add₃ : y * x1 + y * x2 = y * x1 + y * x2
Tactic: rw [add_mul, mul_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
x y : FreeAbelianGroup α
⊢ x * y = y * x
have zero : 0 * y = y * 0
Tactic: induction x using FreeAbelianGroup.induction_on with
    | zero => exact zero_mul y
    | of s =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
    | neg s ih => rw [neg_mul, ih, neg_mul_eq_mul_neg]
    | add x1 x2 ih1 ih2 => rw [add_mul, mul_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
x y : FreeAbelianGroup α
zero : 0 * y = y * 0
⊢ x * y = y * x
have of : ∀ (s : α), of s * y = y * of s
Tactic: induction x using FreeAbelianGroup.induction_on with
    | zero => exact zero_mul y
    | of s =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
    | neg s ih => rw [neg_mul, ih, neg_mul_eq_mul_neg]
    | add x1 x2 ih1 ih2 => rw [add_mul, mul_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
x y : FreeAbelianGroup α
zero : 0 * y = y * 0
of : ∀ (s : α), FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s
⊢ x * y = y * x
have neg : ∀ (s : α) (ih : FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s),
  -FreeAbelianGroup.of s * y = y * -FreeAbelianGroup.of s
Tactic: induction x using FreeAbelianGroup.induction_on with
    | zero => exact zero_mul y
    | of s =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
    | neg s ih => rw [neg_mul, ih, neg_mul_eq_mul_neg]
    | add x1 x2 ih1 ih2 => rw [add_mul, mul_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
x y : FreeAbelianGroup α
zero : 0 * y = y * 0
of : ∀ (s : α), FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s
neg :
  ∀ (s : α) (ih : FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s),
    -FreeAbelianGroup.of s * y = y * -FreeAbelianGroup.of s
⊢ x * y = y * x
have add : ∀ (x1 x2 : FreeAbelianGroup α) (ih1 : x1 * y = y * x1) (ih2 : x2 * y = y * x2), (x1 + x2) * y = y * (x1 + x2)
Tactic: induction x using FreeAbelianGroup.induction_on with
    | zero => exact zero_mul y
    | of s =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
    | neg s ih => rw [neg_mul, ih, neg_mul_eq_mul_neg]
    | add x1 x2 ih1 ih2 => rw [add_mul, mul_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z x y : FreeAbelianGroup T
hx :
  (fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        x) =
    x
hy :
  (fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        y) =
    y
⊢ (fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        (x + y)) =
    x + y
have simp : HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          x :
        ℤ)
      (of default) +
    HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          y :
        ℤ)
      (of default) =
  x + y
Tactic: simp only [map_add, add_smul] at *
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z x y : FreeAbelianGroup T
hx :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          x :
        ℤ)
      (of default) =
    x
hy :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          y :
        ℤ)
      (of default) =
    y
⊢ HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            x :
          ℤ)
        (of default) +
      HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            y :
          ℤ)
        (of default) =
    x + y
have rw : x +
    HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          y :
        ℤ)
      (of default) =
  x + y
Tactic: rw [hx, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z x y : FreeAbelianGroup T
hx :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          x :
        ℤ)
      (of default) =
    x
hy :
  HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          y :
        ℤ)
      (of default) =
    y
rw :
  x +
      HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            y :
          ℤ)
        (of default) =
    x + y
⊢ HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            x :
          ℤ)
        (of default) +
      HSMul.hSMul (α := ℤ) (β := FreeAbelianGroup T)
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
              (a : FreeAbelianGroup T) → ℤ)
            y :
          ℤ)
        (of default) =
    x + y
have rw₁ : x + y = x + y
Tactic: rw [hx, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
n : ℤ
⊢ (((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
        (a : FreeAbelianGroup T) → ℤ)
      ((fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default)) n) =
    n
have rw : HSMul.hSMul (β := ℤ) n 1 = n
Tactic: rw [map_zsmul, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α)
      ((map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) =
    x
have rw : (map (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    x =
  x
Tactic: rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
rw :
  (map (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
⊢ (map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α)
      ((map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) =
    x
have rw₁ : (map id : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
Tactic: rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
rw :
  (map (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
rw₁ : (map id : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
⊢ (map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α)
      ((map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) =
    x
have rw₂ : (AddMonoidHom.id (FreeAbelianGroup α) : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
Tactic: rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
rw :
  (map (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
rw₁ : (map id : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
rw₂ : (AddMonoidHom.id (FreeAbelianGroup α) : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
⊢ (map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α)
      ((map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) =
    x
have rw₃ : x = x
Tactic: rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β)
      ((map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α) x) =
    x
have rw : (map (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := α) (⇑f : (a : α) → β) (⇑f.symm : (a : β) → α)) :
      (a : FreeAbelianGroup β) → FreeAbelianGroup β)
    x =
  x
Tactic: rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
rw :
  (map (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := α) (⇑f : (a : α) → β) (⇑f.symm : (a : β) → α)) :
        (a : FreeAbelianGroup β) → FreeAbelianGroup β)
      x =
    x
⊢ (map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β)
      ((map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α) x) =
    x
have rw₁ : (map id : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
Tactic: rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
rw :
  (map (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := α) (⇑f : (a : α) → β) (⇑f.symm : (a : β) → α)) :
        (a : FreeAbelianGroup β) → FreeAbelianGroup β)
      x =
    x
rw₁ : (map id : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
⊢ (map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β)
      ((map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α) x) =
    x
have rw₂ : (AddMonoidHom.id (FreeAbelianGroup β) : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
Tactic: rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α_1 : Type u
G : Type u_1
β_1 : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
rw :
  (map (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := α) (⇑f : (a : α) → β) (⇑f.symm : (a : β) → α)) :
        (a : FreeAbelianGroup β) → FreeAbelianGroup β)
      x =
    x
rw₁ : (map id : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
rw₂ : (AddMonoidHom.id (FreeAbelianGroup β) : (a : FreeAbelianGroup β) → FreeAbelianGroup β) x = x
⊢ (map (⇑f : (a : α) → β) : (a : FreeAbelianGroup α) → FreeAbelianGroup β)
      ((map (⇑f.symm : (a : β) → α) : (a : FreeAbelianGroup β) → FreeAbelianGroup α) x) =
    x
have rw₃ : x = x
Tactic: rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ (L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length
have rw : L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length
Tactic: rw [List.length_append, List.length_append]