-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem cyclotomicRing_isIntegralClosure_of_prime_pow :
    IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

Proof state:
case refine_1.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
y : ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})
h : IsIntegral ℤ ((algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y)
⊢ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} ⊆ {b | b ^ ↑(p ^ k) = 1}

Tactic:
simp only [PNat.pow_coe, Set.singleton_subset_iff, Set.mem_setOf_eq]

Result:
case refine_1.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
y : ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})
h : IsIntegral ℤ ((algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y)
⊢ zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ) ^ ↑p ^ k = 1

Proof state:
case refine_1
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}

Tactic:
have := isIntegralClosure_adjoin_singleton_of_prime_pow hζ

Result:
case refine_1
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}

Proof state:
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

Tactic:
have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)

Result:
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

Proof state:
case refine_2.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ ((algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y)

Tactic:
exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _).isIntegral _)

Result:
no goals

Proof state:
case refine_2
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
⊢ (∃ y, (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x

Tactic:
rintro ⟨y, rfl⟩

Result:
case refine_2.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ ((algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y)

Proof state:
case refine_1
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}

Tactic:
obtain ⟨y, rfl⟩ := this.isIntegral_iff.1 h

Result:
case refine_1.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
y : ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})
h : IsIntegral ℤ ((algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y)
⊢ (algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y ∈
    adjoin ℤ {b | b ^ ↑(p ^ k) = 1}

Proof state:
case refine_1.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
y : ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})
h : IsIntegral ℤ ((algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y)
⊢ zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ) ^ ↑p ^ k = 1

Tactic:
exact hζ.pow_eq_one

Result:
no goals

Proof state:
case refine_1.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
y : ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})
h : IsIntegral ℤ ((algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y)
⊢ (algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y ∈
    adjoin ℤ {b | b ^ ↑(p ^ k) = 1}

Tactic:
refine adjoin_mono ?_ y.2

Result:
case refine_1.intro
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this : IsIntegralClosure ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)}) ℤ (CyclotomicField (p ^ k) ℚ)
y : ↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})
h : IsIntegral ℤ ((algebraMap (↥(adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)})) (CyclotomicField (p ^ k) ℚ)) y)
⊢ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} ⊆ {b | b ^ ↑(p ^ k) = 1}

Proof state:
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

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

Result:
case refine_1
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}

case refine_2
p : ℕ+
k : ℕ
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
⊢ (∃ y, (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x