case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)

case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
by_cases h' : 1 ≤ p.natDegree
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
⊢ Monic (normalizeScaleRoots p) ∧ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = 0
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
use normalizeScaleRoots p
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
this : p ≠ 0
⊢ Monic (normalizeScaleRoots p) ∧ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = 0
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
⊢ Monic (normalizeScaleRoots p) ∧ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = 0
have : p ≠ 0 := fun h'' => by
  rw [h'', natDegree_zero] at h'
  exact Nat.not_succ_le_zero 0 h'
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
this : p ≠ 0
⊢ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = 0
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
this : p ≠ 0
⊢ Monic (normalizeScaleRoots p) ∧ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = 0
use normalizeScaleRoots_monic p this
no goals
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
this : p ≠ 0
⊢ eval₂ f (↑f (leadingCoeff p) * x) (normalizeScaleRoots p) = 0
rw [normalizeScaleRoots_eval₂_leadingCoeff_mul p h' f x, h, MulZeroClass.mul_zero]
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ 0
h'' : p = 0
⊢ False
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ natDegree p
h'' : p = 0
⊢ False
rw [h'', natDegree_zero] at h'
no goals
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : 1 ≤ 0
h'' : p = 0
⊢ False
exact Nat.not_succ_le_zero 0 h'
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)

case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : ¬Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
by_cases hp : p.map f = 0
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : coeff (Polynomial.map f p) (natDegree p) = coeff 0 (natDegree p)
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
apply_fun fun q => coeff q p.natDegree  at hp
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : ↑f (leadingCoeff p) = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : coeff (Polynomial.map f p) (natDegree p) = coeff 0 (natDegree p)
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
rw [coeff_map, coeff_zero, coeff_natDegree] at hp
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : ↑f (leadingCoeff p) = 0
⊢ IsIntegralElem f 0
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : ↑f (leadingCoeff p) = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
rw [hp, MulZeroClass.zero_mul]
no goals
case pos
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : ↑f (leadingCoeff p) = 0
⊢ IsIntegralElem f 0
exact f.is_integral_zero
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : ¬1 ≤ natDegree p
hp : ¬Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : ↑f (coeff p 0) = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : eval₂ f x p = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : ↑f (coeff p 0) = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
⊢ Polynomial.map f p = 0
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : ↑f (coeff p 0) = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
suffices p.map f = 0 by exact (hp this).elim
no goals
case neg
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : ↑f (coeff p 0) = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
⊢ Polynomial.map f p = 0
rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]
no goals
R : Type u_2
A : Type ?u.952578
B : Type ?u.952581
S : Type u_1
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
h : ↑f (coeff p 0) = 0
h' : natDegree p = 0
hp : ¬Polynomial.map f p = 0
this : Polynomial.map f p = 0
⊢ IsIntegralElem f (↑f (leadingCoeff p) * x)
exact (hp this).elim