-- Mathlib/Algebra/Ring/Center.lean
theorem intCast_mem_center [NonAssocRing M] (n : ℤ) : (n : M) ∈ Set.center M where
  comm _

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑↑n * (x✝¹ * x✝) = ↑↑n * x✝¹ * x✝

Tactic:
rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * ↑(Int.negSucc n) = x✝¹ * (x✝ * ↑(Int.negSucc n))

Tactic:
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]

Result:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * (-1 + -↑n) = x✝¹ * (x✝ * (-1 + -↑n))

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n : ℤ
x✝ : M
⊢ ↑n * x✝ = x✝ * ↑n

Tactic:
rw [Int.commute_cast]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * ↑↑n = x✝¹ * (x✝ * ↑↑n)

Tactic:
rw [Int.cast_natCast, (natCast_mem_center _ n).right_assoc _ _]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * (-1 + -↑n) * x✝ = x✝¹ * ((-1 + -↑n) * x✝)

Tactic:
rw [add_mul, mul_add, add_mul, mul_add, neg_mul, one_mul]

Result:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * -1 * x✝ + x✝¹ * -↑n * x✝ = x✝¹ * -x✝ + x✝¹ * (-↑n * x✝)

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * (↑n * x✝)) = x✝¹ * -x✝ + x✝¹ * -(↑n * x✝)

Tactic:
simp only [mul_neg]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑(Int.negSucc n) * (x✝¹ * x✝) = ↑(Int.negSucc n) * x✝¹ * x✝

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]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * ↑↑n * x✝ = x✝¹ * (↑↑n * x✝)

Tactic:
rw [Int.cast_natCast, (natCast_mem_center _ n).mid_assoc _ _]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * (-1 + -↑n) = x✝¹ * (x✝ * (-1 + -↑n))

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]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * ↑n * x✝) = x✝¹ * -x✝ + x✝¹ * -(↑n * x✝)

Tactic:
rw [(natCast_mem_center _ n).mid_assoc _ _]

Result:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * (↑n * x✝)) = x✝¹ * -x✝ + x✝¹ * -(↑n * x✝)

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * -1 * x✝ + x✝¹ * -↑n * x✝ = x✝¹ * -x✝ + x✝¹ * (-↑n * x✝)

Tactic:
rw [neg_mul, mul_neg, mul_one, mul_neg, neg_mul, neg_mul]

Result:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * ↑n * x✝) = x✝¹ * -x✝ + x✝¹ * -(↑n * x✝)

Proof state:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * ↑(Int.negSucc n) * x✝ = x✝¹ * (↑(Int.negSucc n) * x✝)

Tactic:
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]

Result:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * (-1 + -↑n) * x✝ = x✝¹ * ((-1 + -↑n) * x✝)