R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ ∑ i in Finset.range (natDegree (normalizeScaleRoots p) + 1),
      ↑f (coeff (normalizeScaleRoots p) i) * (↑f (leadingCoeff p) * x) ^ i =
    ∑ x_1 in Finset.range (natDegree p + 1), ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p x_1) * x ^ x_1)
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = ↑f (leadingCoeff p) ^ (natDegree p - 1) * eval₂ f x p
rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]
case h
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ Finset.range (natDegree (normalizeScaleRoots p) + 1) = Finset.range (natDegree p + 1)

case a
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ Finset.range (natDegree p + 1) →
      ↑f (coeff (normalizeScaleRoots p) x_1) * (↑f (leadingCoeff p) * x) ^ x_1 =
        ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p x_1) * x ^ x_1)
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ ∑ i in Finset.range (natDegree (normalizeScaleRoots p) + 1),
      ↑f (coeff (normalizeScaleRoots p) i) * (↑f (leadingCoeff p) * x) ^ i =
    ∑ x_1 in Finset.range (natDegree p + 1), ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p x_1) * x ^ x_1)
apply Finset.sum_congr
case a
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
n : ℕ
_hn : n ∈ Finset.range (natDegree p + 1)
⊢ ↑f (coeff (normalizeScaleRoots p) n) * (↑f (leadingCoeff p) * x) ^ n =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p n) * x ^ n)
case a
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ Finset.range (natDegree p + 1) →
      ↑f (coeff (normalizeScaleRoots p) x_1) * (↑f (leadingCoeff p) * x) ^ x_1 =
        ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p x_1) * x ^ x_1)
intro n _hn
case a
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
n : ℕ
_hn : n ∈ Finset.range (natDegree p + 1)
⊢ ↑f (coeff p n) * ↑f (leadingCoeff p) ^ (natDegree p - 1) * x ^ n =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p n) * x ^ n)
case a
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
n : ℕ
_hn : n ∈ Finset.range (natDegree p + 1)
⊢ ↑f (coeff (normalizeScaleRoots p) n) * (↑f (leadingCoeff p) * x) ^ n =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p n) * x ^ n)
rw [mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
  normalizeScaleRoots_coeff_mul_leadingCoeff_pow _ _ h, f.map_mul, f.map_pow]
no goals
case a
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
n : ℕ
_hn : n ∈ Finset.range (natDegree p + 1)
⊢ ↑f (coeff p n) * ↑f (leadingCoeff p) ^ (natDegree p - 1) * x ^ n =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * (↑f (coeff p n) * x ^ n)
ring
no goals
case h
R : Type u_1
A : Type ?u.888354
B : Type ?u.888357
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
p : R[X]
x✝ : S
h : 1 ≤ natDegree p
f : R →+* S
x : S
⊢ Finset.range (natDegree (normalizeScaleRoots p) + 1) = Finset.range (natDegree p + 1)
rw [natDegree_eq_of_degree_eq (normalizeScaleRoots_degree p)]