-- 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
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))
⊢ (Algebra.norm K) (ζ ^ ↑p ^ k - 1) = ↑↑p ^ ↑p ^ k

Tactic:
by_cases hp : p = 2

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

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

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
⊢ p = 2 → k ≠ 0

Tactic:
rintro rfl rfl

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

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
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
this : ¬↑↑p ^ (k + 1) = 0
⊢ k + 1 ≠ 0

Tactic:
omega

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
H : (aeval ζ) (derivative (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1) = ↑↑(p ^ (k + 1)) * ζ ^ (↑(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 (Algebra.norm K) 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 (minpoly K ζ)) * (ζ ^ ↑p ^ k - 1)) =
    (Algebra.norm K) (↑↑(p ^ (k + 1)) * ζ ^ (↑(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.inl.intro.succ
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)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ ((n✝ + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(2 ^ ((n✝ + 1).succ + 1))
hirr : Irreducible (cyclotomic (↑(2 ^ ((n✝ + 1).succ + 1))) K)
hk : 2 ^ ((n✝ + 1).succ + 1) ≠ 2
hne : NeZero ↑↑(2 ^ ((n✝ + 1).succ + 1))
hp2 : 2 = 2 → (n✝ + 1).succ ≠ 0
⊢ (-1) ^ (2 ^ (n✝ + 1) * (2 * 2 ^ (n✝ + 1) - 1)) = (-1) ^ 2 ^ (n✝ + 1)

Tactic:
simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
  ((even_two.mul_right _).mul_right _).neg_one_pow]

Result:
no goals

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

Tactic:
have hpo : Odd (p : ℕ) := hp.out.odd_of_ne_two hp2

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