awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : ℕ
⊢ x * x_1 * (↑(↑n : ℤ) : M) = x * (x_1 * (↑(↑n : ℤ) : M))
have rw : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
Tactic: rw [Int.cast_natCast, (natCast_mem_center _ n).right_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 : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
⊢ x * x_1 * (↑(↑n : ℤ) : M) = x * (x_1 * (↑(↑n : ℤ) : M))
have rw₁ : x * (x_1 * (↑n : M)) = x * (x_1 * (↑n : M))
Tactic: rw [Int.cast_natCast, (natCast_mem_center _ n).right_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 : ℕ
⊢ x * x_1 * (↑(Int.negSucc n) : M) = x * (x_1 * (↑(Int.negSucc n) : M))
have simp : x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
Tactic: simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]
-- 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 : ℕ
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₈ : -(x * x_1) + -(x * x_1 * (↑n : M)) = -(x * x_1) + x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
rw₈ : -(x * x_1) + -(x * x_1 * (↑n : M)) = -(x * x_1) + x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₉ : -(x * x_1 * (↑n : M)) = x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
rw₈ : -(x * x_1) + -(x * x_1 * (↑n : M)) = -(x * x_1) + x * (x_1 * -(↑n : M))
rw₉ : -(x * x_1 * (↑n : M)) = x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₁₀ : -(x * (x_1 * (↑n : M))) = x * (x_1 * -(↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
rw₈ : -(x * x_1) + -(x * x_1 * (↑n : M)) = -(x * x_1) + x * (x_1 * -(↑n : M))
rw₉ : -(x * x_1 * (↑n : M)) = x * (x_1 * -(↑n : M))
rw₁₀ : -(x * (x_1 * (↑n : M))) = x * (x_1 * -(↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₁₁ : -(x * (x_1 * (↑n : M))) = x * -(x_1 * (↑n : M))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- 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 : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
rw₈ : -(x * x_1) + -(x * x_1 * (↑n : M)) = -(x * x_1) + x * (x_1 * -(↑n : M))
rw₉ : -(x * x_1 * (↑n : M)) = x * (x_1 * -(↑n : M))
rw₁₀ : -(x * (x_1 * (↑n : M))) = x * (x_1 * -(↑n : M))
rw₁₁ : -(x * (x_1 * (↑n : M))) = x * -(x_1 * (↑n : M))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
have rw₁₂ : -(x * (x_1 * (↑n : M))) = -(x * (x_1 * (↑n : M)))
Tactic: rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x : M
⊢ Commute (a + b) x
have rw : (a + b) * x = x * (a + b)
Tactic: rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x : M
rw : (a + b) * x = x * (a + b)
⊢ Commute (a + b) x
have rw₁ : a * x + b * x = x * (a + b)
Tactic: rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x : M
rw : (a + b) * x = x * (a + b)
rw₁ : a * x + b * x = x * (a + b)
⊢ Commute (a + b) x
have rw₂ : a * x + b * x = x * a + x * b
Tactic: rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x : M
rw : (a + b) * x = x * (a + b)
rw₁ : a * x + b * x = x * (a + b)
rw₂ : a * x + b * x = x * a + x * b
⊢ Commute (a + b) x
have rw₃ : x * a + b * x = x * a + x * b
Tactic: rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x : M
rw : (a + b) * x = x * (a + b)
rw₁ : a * x + b * x = x * (a + b)
rw₂ : a * x + b * x = x * a + x * b
rw₃ : x * a + b * x = x * a + x * b
⊢ Commute (a + b) x
have rw₄ : x * a + x * b = x * a + x * b
Tactic: rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
⊢ (a + b) * (x * x_1) = (a + b) * x * x_1
have rw : a * (x * x_1) + b * (x * x_1) = (a + b) * x * x_1
Tactic: rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : a * (x * x_1) + b * (x * x_1) = (a + b) * x * x_1
⊢ (a + b) * (x * x_1) = (a + b) * x * x_1
have rw₁ : a * x * x_1 + b * (x * x_1) = (a + b) * x * x_1
Tactic: rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : a * (x * x_1) + b * (x * x_1) = (a + b) * x * x_1
rw₁ : a * x * x_1 + b * (x * x_1) = (a + b) * x * x_1
⊢ (a + b) * (x * x_1) = (a + b) * x * x_1
have rw₂ : a * x * x_1 + b * x * x_1 = (a + b) * x * x_1
Tactic: rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : a * (x * x_1) + b * (x * x_1) = (a + b) * x * x_1
rw₁ : a * x * x_1 + b * (x * x_1) = (a + b) * x * x_1
rw₂ : a * x * x_1 + b * x * x_1 = (a + b) * x * x_1
⊢ (a + b) * (x * x_1) = (a + b) * x * x_1
have rw₃ : (a * x + b * x) * x_1 = (a + b) * x * x_1
Tactic: rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : a * (x * x_1) + b * (x * x_1) = (a + b) * x * x_1
rw₁ : a * x * x_1 + b * (x * x_1) = (a + b) * x * x_1
rw₂ : a * x * x_1 + b * x * x_1 = (a + b) * x * x_1
rw₃ : (a * x + b * x) * x_1 = (a + b) * x * x_1
⊢ (a + b) * (x * x_1) = (a + b) * x * x_1
have rw₄ : (a + b) * x * x_1 = (a + b) * x * x_1
Tactic: rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
⊢ x * x_1 * (a + b) = x * (x_1 * (a + b))
have rw : x * x_1 * a + x * x_1 * b = x * (x_1 * (a + b))
Tactic: rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : x * x_1 * a + x * x_1 * b = x * (x_1 * (a + b))
⊢ x * x_1 * (a + b) = x * (x_1 * (a + b))
have rw₁ : x * (x_1 * a) + x * x_1 * b = x * (x_1 * (a + b))
Tactic: rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : x * x_1 * a + x * x_1 * b = x * (x_1 * (a + b))
rw₁ : x * (x_1 * a) + x * x_1 * b = x * (x_1 * (a + b))
⊢ x * x_1 * (a + b) = x * (x_1 * (a + b))
have rw₂ : x * (x_1 * a) + x * (x_1 * b) = x * (x_1 * (a + b))
Tactic: rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : x * x_1 * a + x * x_1 * b = x * (x_1 * (a + b))
rw₁ : x * (x_1 * a) + x * x_1 * b = x * (x_1 * (a + b))
rw₂ : x * (x_1 * a) + x * (x_1 * b) = x * (x_1 * (a + b))
⊢ x * x_1 * (a + b) = x * (x_1 * (a + b))
have rw₃ : x * (x_1 * a + x_1 * b) = x * (x_1 * (a + b))
Tactic: rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : x * x_1 * a + x * x_1 * b = x * (x_1 * (a + b))
rw₁ : x * (x_1 * a) + x * x_1 * b = x * (x_1 * (a + b))
rw₂ : x * (x_1 * a) + x * (x_1 * b) = x * (x_1 * (a + b))
rw₃ : x * (x_1 * a + x_1 * b) = x * (x_1 * (a + b))
⊢ x * x_1 * (a + b) = x * (x_1 * (a + b))
have rw₄ : x * (x_1 * (a + b)) = x * (x_1 * (a + b))
Tactic: rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x : M
⊢ Commute (-a) x
have rw : -a * x = x * -a
Tactic: rw [commute_iff_eq, ← neg_mul_comm, ← ha.comm, neg_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x : M
rw : -a * x = x * -a
⊢ Commute (-a) x
have rw₁ : -a * x = -x * a
Tactic: rw [commute_iff_eq, ← neg_mul_comm, ← ha.comm, neg_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x : M
rw : -a * x = x * -a
rw₁ : -a * x = -x * a
⊢ Commute (-a) x
have rw₂ : -a * x = a * -x
Tactic: rw [commute_iff_eq, ← neg_mul_comm, ← ha.comm, neg_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x : M
rw : -a * x = x * -a
rw₁ : -a * x = -x * a
rw₂ : -a * x = a * -x
⊢ Commute (-a) x
have rw₃ : a * -x = a * -x
Tactic: rw [commute_iff_eq, ← neg_mul_comm, ← ha.comm, neg_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
⊢ -a * (x * x_1) = -a * x * x_1
have rw : -(a * (x * x_1)) = -a * x * x_1
Tactic: rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(a * (x * x_1)) = -a * x * x_1
⊢ -a * (x * x_1) = -a * x * x_1
have rw₁ : -(a * x * x_1) = -a * x * x_1
Tactic: rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(a * (x * x_1)) = -a * x * x_1
rw₁ : -(a * x * x_1) = -a * x * x_1
⊢ -a * (x * x_1) = -a * x * x_1
have rw₂ : -(a * x * x_1) = -(a * x) * x_1
Tactic: rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(a * (x * x_1)) = -a * x * x_1
rw₁ : -(a * x * x_1) = -a * x * x_1
rw₂ : -(a * x * x_1) = -(a * x) * x_1
⊢ -a * (x * x_1) = -a * x * x_1
have rw₃ : -(a * x * x_1) = -(a * x * x_1)
Tactic: rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
⊢ x * x_1 * -a = x * (x_1 * -a)
have rw : -(x * x_1 * a) = x * (x_1 * -a)
Tactic: rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(x * x_1 * a) = x * (x_1 * -a)
⊢ x * x_1 * -a = x * (x_1 * -a)
have rw₁ : -(x * (x_1 * a)) = x * (x_1 * -a)
Tactic: rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]