-- 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.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 : IsIntegral ℤ ((algebraMap ℚ K) y)
H : (algebraMap ℚ K) ↑↑p ^ n * (algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : (algebraMap ℚ K) y ∈ ⊥
⊢ (algebraMap ℚ K) y ∈ adjoin ℤ {ζ}

Tactic:
replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h

Result:
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 ℤ {ζ}

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 (algebraMap ℤ ℚ) ((cyclotomic ↑(p ^ (n✝ + 1)) ℤ).comp (X + 1))
⊢ (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {↑↑p})

Tactic:
rw [IsPrimitiveRoot.subOnePowerBasis_gen,
  map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]

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 ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) ((cyclotomic ↑(p ^ (n✝ + 1)) ℤ).comp (X + 1))
⊢ ((cyclotomic ↑(p ^ (n✝ + 1)) ℤ).comp (X + 1)).IsEisensteinAt (Submodule.span ℤ {↑↑p})

Proof state:
case refine_1.intro.intro.succ
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}
hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {↑↑p})
⊢ B.gen ∈ adjoin ℤ {ζ}

Tactic:
exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Result:
no goals

Proof state:
case refine_1.intro.intro
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
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
H : Algebra.discr ℚ ⇑B.basis • x ∈ adjoin ℤ {B.gen}
u : ℤˣ
n : ℕ
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
⊢ x ∈ adjoin ℤ {ζ}

Tactic:
rw [hun] at H

Result:
case refine_1.intro.intro
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
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
H : (↑↑u * ↑↑p ^ n) • x ∈ adjoin ℤ {B.gen}
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
⊢ x ∈ adjoin ℤ {ζ}

Proof state:
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)
⊢ IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K

Tactic:
refine ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩

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
⊢ 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

Proof state:
case refine_1.intro.intro.succ
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}
⊢ x ∈ adjoin ℤ {ζ}

Tactic:
have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {((p : ℕ) : ℤ)}) := by
  have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
  have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)
  rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
  rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
    show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
  rw [IsPrimitiveRoot.subOnePowerBasis_gen,
    map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
  exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _

Result:
case refine_1.intro.intro.succ
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}
hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {↑↑p})
⊢ x ∈ adjoin ℤ {ζ}