-- 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
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 (minpoly K ζ))) * ↑↑p ^ ↑p ^ k =
    ↑↑(p ^ (k + 1)) ^ (↑p ^ k * (↑p - 1)) * (Algebra.norm K) (ζ ^ (↑(p ^ (k + 1)) - 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:
rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow,
  mul_one, PNat.pow_coe, cast_pow, ← pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] 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 + 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))

Proof state:
case neg
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 (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    (Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(p ^ (k + 1)) - 1))
hp : ¬p = 2
⊢ (Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k

Tactic:
exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp

Result:
no goals

Proof state:
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)

Tactic:
rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos,
  Nat.mul_div_cancel_left _ two_pos, mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow,
  pow_mul, hpo.pow.neg_one_pow]

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
hp2 : ↑p ≠ 2
hpo : Odd ↑p
a : ℕ
ha : ↑p - 1 = 2 * a
⊢ Odd (2 * (↑p ^ k * a) - 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.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))

Tactic:
replace H := (mul_left_inj' fun h => ?_).1 H

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

case e_a.refine_1
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)
h : ↑↑p ^ ↑p ^ k = 0
⊢ False

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 ^ k.succ - 1) / 2) = (-1) ^ (2 ^ k.succ / 2)

Tactic:
simp only [_root_.pow_succ']

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