-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem of_smul_isIntegral {y : R} (hy : ¬ IsNilpotent y)
    (h : IsIntegral R (y • z)) : IsAlgebraic R z

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent 0
h✝ : IsIntegral R (0 • z)
eval0 : eval₂ (algebraMap R A) (0 • z) p = 0
h : (p.comp (C 0 * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Tactic:
have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero

Result:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff p.natDegree = coeff 0 p.natDegree
hy0 : y ≠ 0
⊢ False

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent 0
h✝ : IsIntegral R (0 • z)
eval0 : eval₂ (algebraMap R A) (0 • z) p = 0
h : (p.comp (C 0 * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Tactic:
exact hy .zero

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
⊢ (aeval z) (p.comp (C y * X)) = 0

Tactic:
simpa [aeval_comp, Algebra.smul_def] using eval0

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff p.natDegree = coeff 0 p.natDegree
hy0 : y ≠ 0
⊢ False

Tactic:
rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
  coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h

Result:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ 1 ≠ 0

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

Tactic:
exact hy ⟨_, h⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0

Tactic:
rw [natDegree_C_mul_X _ hy0]

Result:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ 1 ≠ 0

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
⊢ IsAlgebraic R z

Tactic:
have ⟨p, monic, eval0⟩ := h

Result:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
⊢ IsAlgebraic R z

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
⊢ IsAlgebraic R z

Tactic:
refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩

Result:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : p.comp (C y * X) = 0
⊢ False