[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
⊢ integralNormalization 0 = 0
[PROOFSTEP]
simp [integralNormalization]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
[PROOFSTEP]
have : f.coeff i = 0 → f.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
this : coeff f i = 0 → degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
[PROOFSTEP]
simp (config := { contextual := true }) [integralNormalization, coeff_monomial, this, mem_support_iff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
⊢ support (integralNormalization f) ⊆ support f
[PROOFSTEP]
intro
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
a✝ : ℕ
⊢ a✝ ∈ support (integralNormalization f) → a✝ ∈ support f
[PROOFSTEP]
simp (config := { contextual := true }) [integralNormalization, coeff_monomial, mem_support_iff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : degree f = ↑i
⊢ coeff (integralNormalization f) i = 1
[PROOFSTEP]
rw [integralNormalization_coeff, if_pos hi]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : degree f ≠ ↑i
⊢ coeff (integralNormalization f) i = coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)
[PROOFSTEP]
rw [integralNormalization_coeff, if_neg hi]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
⊢ support (integralNormalization f) = support f
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : f = 0
⊢ support (integralNormalization f) = support f
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
⊢ support (integralNormalization f) = support f
[PROOFSTEP]
ext i
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support (integralNormalization f) ↔ i ∈ support f
[PROOFSTEP]
refine' ⟨fun h => integralNormalization_support h, _⟩
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support f → i ∈ support (integralNormalization f)
[PROOFSTEP]
simp only [integralNormalization_coeff, mem_support_iff]
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ coeff f i ≠ 0 → (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
[PROOFSTEP]
intro hfi
[GOAL]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
⊢ (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
hi : degree f = ↑i
⊢ 1 ≠ 0
[PROOFSTEP]
simp [hfi, hi, pow_ne_zero _ (leadingCoeff_ne_zero.mpr hf)]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
hi : ¬degree f = ↑i
⊢ coeff f i * leadingCoeff f ^ (natDegree f - 1 - i) ≠ 0
[PROOFSTEP]
simp [hfi, hi, pow_ne_zero _ (leadingCoeff_ne_zero.mpr hf)]
[GOAL]
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
[PROOFSTEP]
rw [eval₂_eq_sum, sum_def, support_integralNormalization]
[GOAL]
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
[PROOFSTEP]
simp only [mul_comm z, mul_pow, mul_assoc, RingHom.map_pow, RingHom.map_mul]
[GOAL]
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)
[PROOFSTEP]
exact Finset.sum_attach.symm
[GOAL]
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
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
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
[PROOFSTEP]
simp [hp]
[GOAL]
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
[PROOFSTEP]
have one_le_deg : 1 ≤ natDegree p := Nat.succ_le_of_lt (natDegree_pos_of_eval₂_root hp f hz inj)
[GOAL]
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
[PROOFSTEP]
congr with i
[GOAL]
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
[PROOFSTEP]
congr 2
[GOAL]
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)
[PROOFSTEP]
by_cases hi : i.1 = natDegree p
[GOAL]
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)
[PROOFSTEP]
rw [hi, integralNormalization_coeff_degree, one_mul, leadingCoeff, ← pow_succ, tsub_add_cancel_of_le one_le_deg]
[GOAL]
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)
[PROOFSTEP]
exact degree_eq_natDegree hp
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
rw [integralNormalization_coeff_ne_natDegree hi, mul_assoc, ← pow_add, tsub_add_cancel_of_le this]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
congr 1
[GOAL]
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
[PROOFSTEP]
exact @Finset.sum_attach _ _ p.support _ fun i => f (p.coeff i) * z ^ i
[GOAL]
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
[PROOFSTEP]
rw [hz, mul_zero]
