-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_eval₂_leadingCoeff_mul_of_commute (h : 1 ≤ p.natDegree) (f : R →+* A)
    (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r'}, Commute (f r) (f r')) :
    (integralNormalization p).eval₂ f (f p.leadingCoeff * x) =
      f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p

Tactic:
rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]

Result:
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ ∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
      f (p.integralNormalization.coeff i) * (f p.leadingCoeff * x) ^ i =
    ∑ i ∈ Finset.range (p.natDegree + 1), f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff i) * x ^ i)

Proof state:
case h
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)

Tactic:
rw [natDegree_eq_of_degree_eq p.integralNormalization_degree]

Result:
no goals

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
⊢ f (p.integralNormalization.coeff n) * (f p.leadingCoeff * x) ^ n =
    f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)

Tactic:
rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
  integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ ∑ i ∈ Finset.range (p.integralNormalization.natDegree + 1),
      f (p.integralNormalization.coeff i) * (f p.leadingCoeff * x) ^ i =
    ∑ i ∈ Finset.range (p.natDegree + 1), f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff i) * x ^ i)

Tactic:
apply Finset.sum_congr

Result:
case h
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ Finset.range (p.integralNormalization.natDegree + 1) = Finset.range (p.natDegree + 1)

case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ ∀ x_1 ∈ Finset.range (p.natDegree + 1),
    f (p.integralNormalization.coeff x_1) * (f p.leadingCoeff * x) ^ x_1 =
      f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff x_1) * x ^ x_1)

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ ∀ x_1 ∈ Finset.range (p.natDegree + 1),
    f (p.integralNormalization.coeff x_1) * (f p.leadingCoeff * x) ^ x_1 =
      f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff x_1) * x ^ x_1)

Tactic:
intro n _hn

Result:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
n : ℕ
_hn : n ∈ Finset.range (p.natDegree + 1)
⊢ f (p.integralNormalization.coeff n) * (f p.leadingCoeff * x) ^ n =
    f p.leadingCoeff ^ (p.natDegree - 1) * (f (p.coeff n) * x ^ n)