-- 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
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
⊢ Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
have : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim := by
  rw [← PowerBasis.finrank, ← PowerBasis.finrank]
  exact RingOfIntegers.rank K

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) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Proof state:
case h.e'_3
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
⊢ (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) =
    (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
simp_rw [algebraMap_int_eq, map_mul, map_pow, map_neg, map_one, map_natCast]

Result:
no goals

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
⊢ (algebraMap (𝓞 K) K) (hζ.toInteger ^ ↑((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Tactic:
convert ← ((IsPrimitiveRoot.powerBasis ℚ hζ).basis_eq_pow i).symm using 1

Result:
no goals

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
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
let pB₁ := integralPowerBasis hζ

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
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

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
⊢ Module.finrank ℤ (𝓞 K) = Module.finrank ℚ K

Tactic:
exact RingOfIntegers.rank K

Result:
no goals

Proof state:
case a
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
⊢ (algebraMap ℤ ℚ) (NumberField.discr K) =
    (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))

Tactic:
rw [← NumberField.discr_eq_discr _ pB₁.basis, ← Algebra.discr_localizationLocalization ℤ ℤ⁰ K]

Result:
case a
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
⊢ Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) =
    (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))

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
⊢ NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
apply (algebraMap ℤ ℚ).injective_int

Result:
case a
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
⊢ (algebraMap ℤ ℚ) (NumberField.discr K) =
    (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))

Proof state:
case a
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
⊢ Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) =
    (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))

Tactic:
convert IsCyclotomicExtension.discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).2) using 1

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
⊢ Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

case h.e'_3
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
⊢ (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) =
    (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

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) ∘ ⇑(finCongr this).symm) =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
congr 1

Result:
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