-- Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis K L}
    (hp : Prime p) (hBint : IsIntegral R B.gen) {z : L} (hzint : IsIntegral R z)
    (hz : p • z ∈ adjoin R ({B.gen} : Set L)) (hei : (minpoly R B.gen).IsEisensteinAt 𝓟) :
    z ∈ adjoin R ({B.gen} : Set L)

Proof state:
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
hQ : (aeval B.gen).toRingHom (Q₁ %ₘ minpoly R B.gen + minpoly R B.gen * (Q₁ /ₘ minpoly R B.gen)) = p • z
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
⊢ (aeval B.gen) Q = p • z

Tactic:
simpa using hQ

Result:
no goals

Proof state:
case neg.hi.convert_2
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : (Q₁ %ₘ minpoly R B.gen).degree < (minpoly R B.gen).degree
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n

Tactic:
rw [← hQ₁, ← hP] at H

Result:
case neg.hi.convert_2
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : Q.degree < P.degree
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n

Proof state:
case intro.intro
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
hQ : (aeval B.gen).toRingHom Q₁ = p • z
⊢ z ∈ adjoin R {B.gen}

Tactic:
set Q := Q₁ %ₘ P with hQ₁

Result:
case intro.intro
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
hQ : (aeval B.gen).toRingHom Q₁ = p • z
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
⊢ z ∈ adjoin R {B.gen}

Proof state:
case neg.hi
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
⊢ p ∣ Q.coeff (j + 1)

Tactic:
convert hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) _ hndiv

Result:
case neg.hi.convert_2
R : Type u
K : Type v
L : Type z
p : R
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (Submodule.span R {p})
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : NoZeroSMulDivisors R L
x✝ : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n