-- 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:
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
⊢ (-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))

Tactic:
have hp2 : p = 2 → k ≠ 0 := by
  rintro rfl rfl
  exact absurd rfl hk

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
coe_two : ↑2 = 2
hp2 : p = 2 → k ≠ 0
⊢ (-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
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
have H := congr_arg (@derivative K _) (cyclotomic_prime_pow_mul_X_pow_sub_one K p k)

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 : derivative (cyclotomic (↑p ^ (k + 1)) K * (X ^ ↑p ^ k - 1)) = derivative (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:
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))
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
haveI mf : Module.Finite K L := finiteDimensional {p ^ (k + 1)} K L

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
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Proof state:
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)
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (0 + 1))) K)
hk : 2 ^ (0 + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (0 + 1))
⊢ False

Tactic:
exact absurd rfl hk

Result:
no goals

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

Tactic:
rcases eq_or_ne p 2 with (rfl | hp2)

Result:
case e_a.inl
k : ℕ
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
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑2)
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)
hk : 2 ^ (k + 1) ≠ 2
hne : NeZero ↑↑(2 ^ (k + 1))
hp2 : 2 = 2 → k ≠ 0
⊢ (-1) ^ (↑2 ^ k * (↑2 - 1) * (↑2 ^ k * (↑2 - 1) - 1) / 2) = (-1) ^ (↑2 ^ k * (↑2 - 1) / 2)

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
⊢ (-1) ^ (↑p ^ k * (↑p - 1) * (↑p ^ k * (↑p - 1) - 1) / 2) = (-1) ^ (↑p ^ k * (↑p - 1) / 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 :
  (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
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (↑p ^ (k + 1)) K))) = ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)

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 + 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))