R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
⊢ (if coeff p i = 0 then 0
    else
      if i = natDegree p then leadingCoeff p ^ i
      else coeff p i * leadingCoeff p ^ (natDegree p - 1 - i) * leadingCoeff p ^ i) =
    coeff p i * leadingCoeff p ^ (natDegree p - 1)
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
⊢ coeff (normalizeScaleRoots p) i * leadingCoeff p ^ i = coeff p i * leadingCoeff p ^ (natDegree p - 1)
simp only [normalizeScaleRoots, finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', one_mul,
  MulZeroClass.zero_mul, mem_support_iff, ite_mul, Ne.def, ite_not]
case inl
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : coeff p i = 0
⊢ 0 = coeff p i * leadingCoeff p ^ (natDegree p - 1)

case inr.inl
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : i = natDegree p
⊢ leadingCoeff p ^ i = coeff p i * leadingCoeff p ^ (natDegree p - 1)

case inr.inr
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ coeff p i * leadingCoeff p ^ (natDegree p - 1 - i) * leadingCoeff p ^ i =
    coeff p i * leadingCoeff p ^ (natDegree p - 1)
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
⊢ (if coeff p i = 0 then 0
    else
      if i = natDegree p then leadingCoeff p ^ i
      else coeff p i * leadingCoeff p ^ (natDegree p - 1 - i) * leadingCoeff p ^ i) =
    coeff p i * leadingCoeff p ^ (natDegree p - 1)
split_ifs with h₁ h₂
no goals
case inl
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : coeff p i = 0
⊢ 0 = coeff p i * leadingCoeff p ^ (natDegree p - 1)
simp [h₁]
no goals
case inr.inl
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : i = natDegree p
⊢ leadingCoeff p ^ i = coeff p i * leadingCoeff p ^ (natDegree p - 1)
rw [h₂, leadingCoeff, ← pow_succ, tsub_add_cancel_of_le hp]
case inr.inr
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ i ≤ natDegree p - 1
case inr.inr
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ coeff p i * leadingCoeff p ^ (natDegree p - 1 - i) * leadingCoeff p ^ i =
    coeff p i * leadingCoeff p ^ (natDegree p - 1)
rw [mul_assoc, ← pow_add, tsub_add_cancel_of_le]
case inr.inr.h
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ i < natDegree p
case inr.inr
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ i ≤ natDegree p - 1
apply Nat.le_pred_of_lt
case inr.inr.h
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ i ≤ natDegree p ∧ i ≠ natDegree p
case inr.inr.h
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ i < natDegree p
rw [lt_iff_le_and_ne]
no goals
case inr.inr.h
R : Type u_1
A : Type ?u.865622
B : Type ?u.865625
S : Type ?u.865628
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
i : ℕ
hp : 1 ≤ natDegree p
h₁ : ¬coeff p i = 0
h₂ : ¬i = natDegree p
⊢ i ≤ natDegree p ∧ i ≠ natDegree p
exact ⟨le_natDegree_of_ne_zero h₁, h₂⟩