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

Proof state:
case zero
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
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
hz : p ^ 0 • z ∈ adjoin R {B.gen}
⊢ z ∈ adjoin R {B.gen}

Tactic:
simpa using hz

Result:
no goals

Proof state:
case succ
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
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
n : ℕ
hn : p ^ n • z ∈ adjoin R {B.gen} → z ∈ adjoin R {B.gen}
hz : p ^ (n + 1) • z ∈ adjoin R {B.gen}
⊢ z ∈ adjoin R {B.gen}

Tactic:
rw [_root_.pow_succ', mul_smul] at hz

Result:
case succ
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
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
n : ℕ
hn : p ^ n • z ∈ adjoin R {B.gen} → z ∈ adjoin R {B.gen}
hz : p • p ^ n • z ∈ adjoin R {B.gen}
⊢ z ∈ adjoin R {B.gen}

Proof state:
case succ
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
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
n : ℕ
hn : p ^ n • z ∈ adjoin R {B.gen} → z ∈ adjoin R {B.gen}
hz : p • p ^ n • z ∈ adjoin R {B.gen}
⊢ z ∈ adjoin R {B.gen}

Tactic:
exact
  hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)

Result:
no goals

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
n : ℕ
z : L
hzint : IsIntegral R z
hz : p ^ n • z ∈ adjoin R {B.gen}
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
⊢ z ∈ adjoin R {B.gen}

Tactic:
induction' n with n hn

Result:
case zero
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
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
hz : p ^ 0 • z ∈ adjoin R {B.gen}
⊢ z ∈ adjoin R {B.gen}

case succ
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
hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})
n : ℕ
hn : p ^ n • z ∈ adjoin R {B.gen} → z ∈ adjoin R {B.gen}
hz : p ^ (n + 1) • z ∈ adjoin R {B.gen}
⊢ z ∈ adjoin R {B.gen}