R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
⊢ x ∈ support (normalizeScaleRoots p) → x ∈ support p
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
⊢ support (normalizeScaleRoots p) ≤ support p
intro x
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
⊢ ¬x ∈ support p → ¬x ∈ support (normalizeScaleRoots p)
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
⊢ x ∈ support (normalizeScaleRoots p) → x ∈ support p
contrapose
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
⊢ coeff p x = 0 →
    ¬coeff p x = 0 → (if x = natDegree p then 1 else coeff p x * leadingCoeff p ^ (natDegree p - 1 - x)) = 0
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
⊢ ¬x ∈ support p → ¬x ∈ support (normalizeScaleRoots p)
simp only [not_mem_support_iff, normalizeScaleRoots, finset_sum_coeff, coeff_monomial,
  Finset.sum_ite_eq', mem_support_iff, Ne.def, Classical.not_not, ite_eq_right_iff]
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
h₁ : coeff p x = 0
h₂ : ¬coeff p x = 0
⊢ (if x = natDegree p then 1 else coeff p x * leadingCoeff p ^ (natDegree p - 1 - x)) = 0
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
⊢ coeff p x = 0 →
    ¬coeff p x = 0 → (if x = natDegree p then 1 else coeff p x * leadingCoeff p ^ (natDegree p - 1 - x)) = 0
intro h₁ h₂
no goals
R : Type u_1
A : Type ?u.882928
B : Type ?u.882931
S : Type ?u.882934
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
x : ℕ
h₁ : coeff p x = 0
h₂ : ¬coeff p x = 0
⊢ (if x = natDegree p then 1 else coeff p x * leadingCoeff p ^ (natDegree p - 1 - x)) = 0
exact (h₂ h₁).elim