-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_eval₂_eq_zero_of_commute {p : R[X]} (f : R →+* A) {z : A}
    (hz : eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r'}, Commute (f r) (f r'))
    (inj : ∀ x : R, f x = 0 → x = 0) :
    eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h]

Result:
case pos
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (f (C (p.coeff 0)).leadingCoeff * z) (C (p.coeff 0)).integralNormalization = 0

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : f (p.coeff 0) = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
exact absurd (inj _ hz) h0

Result:
no goals

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
by_cases h0 : coeff p 0 = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (f (C (p.coeff 0)).leadingCoeff * z) (C (p.coeff 0)).integralNormalization = 0

Tactic:
simp [h0]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree > 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
obtain (h | h) := p.natDegree.eq_zero_or_pos

Result:
case inl
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

case inr
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree > 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

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

Result:
case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : f (p.coeff 0) = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0