case a
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
⊢ coeff (leadingCoeff p • normalizeScaleRoots p) n✝ = coeff (scaleRoots p (leadingCoeff p)) n✝
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
⊢ leadingCoeff p • normalizeScaleRoots p = scaleRoots p (leadingCoeff p)
ext
case a
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
⊢ (∑ x in support p,
      leadingCoeff p •
        if x = n✝ then if x = natDegree p then 1 else coeff p x * leadingCoeff p ^ (natDegree p - 1 - x) else 0) =
    coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
case a
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
⊢ coeff (leadingCoeff p • normalizeScaleRoots p) n✝ = coeff (scaleRoots p (leadingCoeff p)) n✝
simp only [coeff_scaleRoots, normalizeScaleRoots, coeff_monomial, coeff_smul, Finset.smul_sum,
  Ne.def, Finset.sum_ite_eq', finset_sum_coeff, smul_ite, smul_zero, mem_support_iff]
case a
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
⊢ (if coeff p n✝ = 0 then 0
    else
      if n✝ = natDegree p then leadingCoeff p
      else leadingCoeff p * (coeff p n✝ * leadingCoeff p ^ (natDegree p - 1 - n✝))) =
    coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
case a
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
⊢ (∑ x in support p,
      leadingCoeff p •
        if x = n✝ then if x = natDegree p then 1 else coeff p x * leadingCoeff p ^ (natDegree p - 1 - x) else 0) =
    coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
simp only [ge_iff_le, tsub_le_iff_right, smul_eq_mul, mul_ite, mul_one, mul_zero,
  Finset.sum_ite_eq', mem_support_iff, ne_eq, ite_not]
case a.inl
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : coeff p n✝ = 0
⊢ 0 = coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)

case a.inr.inl
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : n✝ = natDegree p
⊢ leadingCoeff p = coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)

case a.inr.inr
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : ¬n✝ = natDegree p
⊢ leadingCoeff p * (coeff p n✝ * leadingCoeff p ^ (natDegree p - 1 - n✝)) =
    coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
case a
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
⊢ (if coeff p n✝ = 0 then 0
    else
      if n✝ = natDegree p then leadingCoeff p
      else leadingCoeff p * (coeff p n✝ * leadingCoeff p ^ (natDegree p - 1 - n✝))) =
    coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
split_ifs with h₁ h₂
no goals
case a.inl
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : coeff p n✝ = 0
⊢ 0 = coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
simp [*]
no goals
case a.inr.inl
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : n✝ = natDegree p
⊢ leadingCoeff p = coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
simp [*]
case a.inr.inr
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : ¬n✝ = natDegree p
⊢ 1 ≤ natDegree p - n✝
case a.inr.inr
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : ¬n✝ = natDegree p
⊢ leadingCoeff p * (coeff p n✝ * leadingCoeff p ^ (natDegree p - 1 - n✝)) =
    coeff p n✝ * leadingCoeff p ^ (natDegree p - n✝)
rw [mul_comm, mul_assoc, ← pow_succ', tsub_right_comm,
  tsub_add_cancel_of_le]
case a.inr.inr
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : ¬n✝ = natDegree p
⊢ 0 < natDegree p - n✝
case a.inr.inr
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : ¬n✝ = natDegree p
⊢ 1 ≤ natDegree p - n✝
rw [Nat.succ_le_iff]
no goals
case a.inr.inr
R : Type u_1
A : Type ?u.873552
B : Type ?u.873555
S : Type ?u.873558
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
p : R[X]
n✝ : ℕ
h₁ : ¬coeff p n✝ = 0
h₂ : ¬n✝ = natDegree p
⊢ 0 < natDegree p - n✝
exact tsub_pos_of_lt (lt_of_le_of_ne (le_natDegree_of_ne_zero h₁) h₂)