-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K

Proof state:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
⊢ x ∈ adjoin ℤ {ζ}

Tactic:
have hint : IsIntegral ℤ B.gen := (hζ.isIntegral (p ^ k).pos).sub isIntegral_one

Result:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
⊢ x ∈ adjoin ℤ {ζ}

Proof state:
case refine_1.intro.intro.zero.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑↑p ^ n * (algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
⊢ (algebraMap ℚ K) y ∈ adjoin ℤ {ζ}

Tactic:
obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h

Result:
case refine_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑↑p ^ n * (algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ) z = y
⊢ (algebraMap ℚ K) y ∈ adjoin ℤ {ζ}

Proof state:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {ζ}

case refine_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
⊢ (∃ y, (algebraMap (↥(adjoin ℤ {ζ})) K) y = x) → IsIntegral ℤ x

Tactic:
swap

Result:
case refine_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
⊢ (∃ y, (algebraMap (↥(adjoin ℤ {ζ})) K) y = x) → IsIntegral ℤ x

case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {ζ}

Proof state:
case refine_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑↑p ^ n * (algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ) z = y
⊢ (algebraMap ℚ K) y ∈ adjoin ℤ {ζ}

Tactic:
rw [← hz, ← IsScalarTower.algebraMap_apply]

Result:
case refine_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑↑p ^ n * (algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ) z = y
⊢ (algebraMap ℤ K) z ∈ adjoin ℤ {ζ}

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
H : (algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = (map (Int.castRingHom ℚ) (cyclotomic ↑(p ^ (n✝ + 1)) ℤ)).comp (X + 1)
⊢ Int.castRingHom ℚ = algebraMap ℤ ℚ

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑↑p ^ n * (algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ) z = y
⊢ (algebraMap ℤ K) z ∈ adjoin ℤ {ζ}

Tactic:
exact Subalgebra.algebraMap_mem _ _

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
H : (algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
⊢ (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {↑↑p})

Tactic:
have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
H : (algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
h₂ : minpoly ℚ (ζ - 1) = (cyclotomic ↑(p ^ (n✝ + 1)) ℚ).comp (X + 1)
⊢ (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {↑↑p})