awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₂ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ₃ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M) + x_1 * 1)
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₂ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₃ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M) + x_1 * 1)
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ₄ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₂ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₃ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M) + x_1 * 1)
succ₄ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ₅ : x * (x_1 * (↑n : M)) + x * x_1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₂ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₃ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M) + x_1 * 1)
succ₄ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
succ₅ : x * (x_1 * (↑n : M)) + x * x_1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
have succ₆ : x * (x_1 * (↑n : M)) + x * x_1 = x * (x_1 * (↑n : M)) + x * x_1
Tactic: rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x x_1 : M
⊢ x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
have zero : x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
Tactic: induction n with
    | zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
    | succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x x_1 : M
zero : x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
⊢ x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
have succ : ∀ (n : ℕ) (ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))), x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
Tactic: induction n with
    | zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
    | succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n : ℤ
x : M
⊢ Commute (↑n : M) x
have rw : (↑n : M) * x = x * (↑n : M)
Tactic: rw [commute_iff_eq, Int.commute_cast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n : ℤ
x : M
rw : (↑n : M) * x = x * (↑n : M)
⊢ Commute (↑n : M) x
have rw₁ : (↑n : M) * x = (↑n : M) * x
Tactic: rw [commute_iff_eq, Int.commute_cast]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
⊢ (↑(↑n : ℤ) : M) * (x * x_1) = (↑(↑n : ℤ) : M) * x * x_1
have rw : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
Tactic: rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
⊢ (↑(↑n : ℤ) : M) * (x * x_1) = (↑(↑n : ℤ) : M) * x * x_1
have rw₁ : (↑n : M) * x * x_1 = (↑n : M) * x * x_1
Tactic: rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁₁ : -x * x_1 + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₁ : -x * x_1 + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁₂ : -(↑n : M) * (x * x_1) = -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₁ : -x * x_1 + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₂ : -(↑n : M) * (x * x_1) = -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁₃ : -((↑n : M) * (x * x_1)) = -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₁ : -x * x_1 + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₂ : -(↑n : M) * (x * x_1) = -(↑n : M) * x * x_1
rw₁₃ : -((↑n : M) * (x * x_1)) = -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁₄ : -((↑n : M) * x * x_1) = -(↑n : M) * x * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₁ : -x * x_1 + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₂ : -(↑n : M) * (x * x_1) = -(↑n : M) * x * x_1
rw₁₃ : -((↑n : M) * (x * x_1)) = -(↑n : M) * x * x_1
rw₁₄ : -((↑n : M) * x * x_1) = -(↑n : M) * x * x_1
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1
have rw₁₅ : -((↑n : M) * x * x_1) = -((↑n : M) * x) * x_1
Tactic: rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]