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

Proof state:
case e_a.refine_2
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
hnorm : (Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < k.succ * (↑p - 1)
H : (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * (k.succ * (↑p - 1)).pred)
⊢ ↑↑p ^ (↑p ^ k * (k.succ * (↑p - 1)).pred) = ↑↑p ^ (↑p ^ k * ((k + 1) * (↑p - 1) - 1))

Tactic:
norm_cast

Result:
no goals

Proof state:
case e_a.inl.intro
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (k.succ + 1))) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (↑2 ^ k.succ * (↑2 - 1) * (↑2 ^ k.succ * (↑2 - 1) - 1) / 2) = (-1) ^ (↑2 ^ k.succ * (↑2 - 1) / 2)

Tactic:
rw [coe_two, succ_sub_succ_eq_sub, tsub_zero, mul_one]

Result:
case e_a.inl.intro
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp : Fact (Nat.Prime ↑2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (k.succ + 1))) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 ^ k.succ * (2 ^ k.succ - 1) / 2) = (-1) ^ (2 ^ k.succ / 2)

Proof state:
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  derivative (minpoly K ζ) * (X ^ ↑p ^ k - 1) + minpoly K ζ * (↑(↑p ^ k) * X ^ (↑p ^ k - 1)) =
    ↑↑(p ^ (k + 1)) * X ^ (↑(p ^ (k + 1)) - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
replace H := congr_arg (fun P => aeval ζ P) H

Result:
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  (fun P => (aeval ζ) P) (derivative (minpoly K ζ) * (X ^ ↑p ^ k - 1) + minpoly K ζ * (↑(↑p ^ k) * X ^ (↑p ^ k - 1))) =
    (fun P => (aeval ζ) P) (↑↑(p ^ (k + 1)) * X ^ (↑(p ^ (k + 1)) - 1))
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Proof state:
case e_a.inr
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = (-1) ^ (↑p ^ k * (↑p - 1) / 2)

Tactic:
obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd

Result:
case e_a.inr.intro
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2✝ : p = 2 → k ≠ 0
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = (-1) ^ (↑p ^ k * (↑p - 1) / 2)

Proof state:
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
rw [discr_powerBasis_eq_norm, finrank L hirr, hζ.powerBasis_gen _, ←
  hζ.minpoly_eq_cyclotomic_of_irreducible hirr, PNat.pow_coe,
  totient_prime_pow hp.out (succ_pos k), Nat.add_one_sub_one]

Result:
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) *
      (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) =
    (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Proof state:
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * ((k + 1) * (↑p - 1)))
hnorm : (Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < k.succ * (↑p - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ ((p : ℕ) ^ k)] at H

Result:
case e_a
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) * ↑↑p ^ ↑p ^ k =
    ↑↑p ^ (↑p ^ k * (k.succ * (↑p - 1)).pred) * ↑↑p ^ ↑p ^ k
hnorm : (Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k
this : 0 < k.succ * (↑p - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))