-- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (p : ℕ).Prime]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (hirr : Irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
    discr K (hζ.powerBasis K).basis =
      (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1))

Proof state:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    (-1) ^ (φ (↑2 ^ (0 + 1)) / 2) * ↑↑2 ^ (↑2 ^ (0 + 1 - 1) * ((↑2 - 1) * (0 + 1) - 1))

Tactic:
have : natDegree (minpoly K ζ) = 1 := by
  rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
    minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]
  exact natDegree_X_sub_C (-1)

Result:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    (-1) ^ (φ (↑2 ^ (0 + 1)) / 2) * ↑↑2 ^ (↑2 ^ (0 + 1 - 1) * ((↑2 - 1) * (0 + 1) - 1))

Proof state:
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
hirr : Irreducible (cyclotomic (↑(p ^ 0)) K)
hζone : ζ = 1
⊢ Matrix.of (fun i j => (trace K L) 1) default default = 1 * ↑↑p ^ (↑p ^ (0 - 1) * (0 - 1))

Tactic:
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]

Result:
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
hirr : Irreducible (cyclotomic (↑(p ^ 0)) K)
hζone : ζ = 1
⊢ Matrix.of (fun i j => φ ↑(p ^ 0) • 1) default default = 1 * ↑↑p ^ (↑p ^ (0 - 1) * (0 - 1))

Proof state:
case pos.intro
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i => (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) = 1

Tactic:
convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _

Result:
case h.e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i => (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) = discr K fun i => (algebraMap K L) (-1) ^ ↑i

case pos.intro.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (discr K fun i => (algebraMap K L) (-1) ^ ↑i) = 1

Proof state:
case pos.intro.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (trace K L) 1 = 1

Tactic:
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]

Result:
case pos.intro.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ φ ↑(2 ^ (0 + 1)) • 1 = 1

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
hirr : Irreducible (cyclotomic (↑(p ^ 0)) K)
⊢ ζ = 1

Tactic:
simpa using hζ

Result:
no goals

Proof state:
case pos.intro
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    (-1) ^ (φ (↑2 ^ (0 + 1)) / 2) * ↑↑2 ^ (↑2 ^ (0 + 1 - 1) * ((↑2 - 1) * (0 + 1) - 1))

Tactic:
rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]

Result:
case pos.intro
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i => ζ ^ ↑i) ∘ ⇑e.symm) =
    (-1) ^ (φ (↑2 ^ (0 + 1)) / 2) * ↑↑2 ^ (↑2 ^ (0 + 1 - 1) * ((↑2 - 1) * (0 + 1) - 1))

Proof state:
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this✝ : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
this : ↑(e.symm i) = 0
⊢ (-1) ^ ↑(e.symm i) = 1

Tactic:
simp [this]

Result:
no goals

Proof state:
case h.e'_2.e_b.h
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ↑(e.symm i) < 1

Tactic:
convert (e.symm i).2

Result:
case h.e'_4
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
coe_two : 2 = ↑2
hp : Fact (Nat.Prime ↑2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ ↑2
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ 1 = (minpoly K ζ).natDegree