-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem absdiscr_prime_pow [IsCyclotomicExtension {p ^ k} ℚ K] :
    haveI : NumberField K := IsCyclotomicExtension.numberField {p ^ k} ℚ K
    NumberField.discr K =
    (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1))

Proof state:
case h.e'_2.e_b.h
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) ∘ ⇑(finCongr this).symm) i =
    (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Tactic:
simp_rw [Function.comp_apply, Basis.localizationLocalization_apply, powerBasis_dim,
  PowerBasis.coe_basis, pB₁, integralPowerBasis_gen]

Result:
case h.e'_2.e_b.h
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (algebraMap (𝓞 K) K) (hζ.toInteger ^ ↑((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ k} ℚ K

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this : NumberField K
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Proof state:
case h.e'_2.e_b
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) ∘ ⇑(finCongr this).symm = ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
ext i

Result:
case h.e'_2.e_b.h
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) ∘ ⇑(finCongr this).symm) i =
    (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Proof state:
case h.e'_2
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
rw [← Algebra.discr_reindex _ _ (finCongr this)]

Result:
case h.e'_2
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ Algebra.discr ℚ (⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) ∘ ⇑(finCongr this).symm) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
⊢ pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim

Tactic:
rw [← PowerBasis.finrank, ← PowerBasis.finrank]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
⊢ Module.finrank ℤ (𝓞 K) = Module.finrank ℚ K

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec (p ^ k) ℚ K

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))