-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem RingHom.isIntegralElem_leadingCoeff_mul (h : p.eval₂ f x = 0) :
    f.IsIntegralElem (f p.leadingCoeff * x)

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
by_cases h' : 1 ≤ p.natDegree

Result:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ 0
h'' : p = 0
⊢ False

Tactic:
exact Nat.not_succ_le_zero 0 h'

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h

Result:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Proof state:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
use integralNormalization p

Result:
case h
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Proof state:
case h
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Tactic:
have : p ≠ 0 := fun h'' => by
  rw [h'', natDegree_zero] at h'
  exact Nat.not_succ_le_zero 0 h'

Result:
case h
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Proof state:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
by_cases hp : p.map f = 0

Result:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h'' : p = 0
⊢ False

Tactic:
rw [h'', natDegree_zero] at h'

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ 0
h'' : p = 0
⊢ False

Proof state:
case right
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Tactic:
rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]

Result:
no goals

Proof state:
case h
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Tactic:
use monic_integralNormalization this

Result:
case right
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
this : Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
exact (hp this).elim

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ Polynomial.map f p = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]

Result:
no goals

Proof state:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
apply_fun fun q => coeff q p.natDegree at hp

Result:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : (Polynomial.map f p).coeff p.natDegree = coeff 0 p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Proof state:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem 0

Tactic:
exact f.isIntegralElem_zero

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
suffices p.map f = 0 by exact (hp this).elim

Result:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ Polynomial.map f p = 0

Proof state:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
rw [hp, zero_mul]

Result:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem 0

Proof state:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : (Polynomial.map f p).coeff p.natDegree = coeff 0 p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
rw [coeff_map, coeff_zero, coeff_natDegree] at hp

Result:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : f p.leadingCoeff = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Proof state:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'

Result:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)