R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ n in support p, ↑f (coeff (integralNormalization p) n) * (z * ↑f (leadingCoeff p)) ^ n =
    ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ eval₂ f (z * ↑f (leadingCoeff p)) (integralNormalization p) =
    ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i
rw [eval₂_eq_sum, sum_def, support_integralNormalization]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ x in support p, ↑f (coeff (integralNormalization p) x) * (↑f (leadingCoeff p) ^ x * z ^ x) =
    ∑ x in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑x) * (↑f (leadingCoeff p) ^ ↑x * z ^ ↑x)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ n in support p, ↑f (coeff (integralNormalization p) n) * (z * ↑f (leadingCoeff p)) ^ n =
    ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i
simp only [mul_comm z, mul_pow, mul_assoc, RingHom.map_pow, RingHom.map_mul]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ x in support p, ↑f (coeff (integralNormalization p) x) * (↑f (leadingCoeff p) ^ x * z ^ x) =
    ∑ x in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑x) * (↑f (leadingCoeff p) ^ ↑x * z ^ ↑x)
exact Finset.sum_attach.symm
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : p = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
by_cases hp : p = 0
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
have one_le_deg : 1 ≤ natDegree p :=
  Nat.succ_le_of_lt (natDegree_pos_of_eval₂_root hp f hz inj)
case neg.e_f.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
⊢ ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
congr with i
case neg.e_f.h.e_a.h.e_6.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
case neg.e_f.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
⊢ ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
congr 2
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ↑i = natDegree p
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ¬↑i = natDegree p
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
case neg.e_f.h.e_a.h.e_6.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
by_cases hi : i.1 = natDegree p
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : p = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i) * z ^ ↑i =
    ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i
simp [hp]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ↑i = natDegree p
⊢ degree p = ↑(natDegree p)
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ↑i = natDegree p
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
rw [hi, integralNormalization_coeff_degree, one_mul, leadingCoeff, ← pow_succ,
  tsub_add_cancel_of_le one_le_deg]
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ↑i = natDegree p
⊢ degree p = ↑(natDegree p)
exact degree_eq_natDegree hp
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ¬↑i = natDegree p
this : ↑i ≤ natDegree p - 1
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ¬↑i = natDegree p
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
have : i.1 ≤ p.natDegree - 1 :=
  Nat.le_pred_of_lt (lt_of_le_of_ne (le_natDegree_of_ne_zero (mem_support_iff.mp i.2)) hi)
no goals
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hp : ¬p = 0
one_le_deg : 1 ≤ natDegree p
i : { x // x ∈ support p }
hi : ¬↑i = natDegree p
this : ↑i ≤ natDegree p - 1
⊢ coeff (integralNormalization p) ↑i * leadingCoeff p ^ ↑i = coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)
rw [integralNormalization_coeff_ne_natDegree hi, mul_assoc, ← pow_add,
  tsub_add_cancel_of_le this]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ↑f (leadingCoeff p) ^ (natDegree p - 1) * ∑ x in Finset.attach (support p), ↑f (coeff p ↑x) * z ^ ↑x =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * ∑ n in support p, ↑f (coeff p n) * z ^ n
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ i in Finset.attach (support p), ↑f (coeff p ↑i * leadingCoeff p ^ (natDegree p - 1)) * z ^ ↑i =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * eval₂ f z p
simp_rw [eval₂_eq_sum, sum_def, fun i => mul_comm (coeff p i), RingHom.map_mul,
         RingHom.map_pow, mul_assoc, ← Finset.mul_sum]
case e_a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ x in Finset.attach (support p), ↑f (coeff p ↑x) * z ^ ↑x = ∑ n in support p, ↑f (coeff p n) * z ^ n
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ↑f (leadingCoeff p) ^ (natDegree p - 1) * ∑ x in Finset.attach (support p), ↑f (coeff p ↑x) * z ^ ↑x =
    ↑f (leadingCoeff p) ^ (natDegree p - 1) * ∑ n in support p, ↑f (coeff p n) * z ^ n
congr 1
no goals
case e_a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ∑ x in Finset.attach (support p), ↑f (coeff p ↑x) * z ^ ↑x = ∑ n in support p, ↑f (coeff p n) * z ^ n
exact @Finset.sum_attach _ _ p.support _ fun i => f (p.coeff i) * z ^ i
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CommSemiring S
p : R[X]
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
⊢ ↑f (leadingCoeff p) ^ (natDegree p - 1) * eval₂ f z p = 0
rw [hz, mul_zero]