-- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
theorem discr_prime_pow_eq_unit_mul_pow [IsCyclotomicExtension {p ^ k} K L]
    [hp : Fact (p : ℕ).Prime] (hζ : IsPrimitiveRoot ζ ↑(p ^ k))
    (hirr : Irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
    ∃ (u : ℤˣ) (n : ℕ), discr K (hζ.powerBasis K).basis = u * p ^ n

Proof state:
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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ (↑p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n

Tactic:
exact ⟨1, (p : ℕ) ^ (k - 1) * ((p - 1) * k - 1), by rw [heven.neg_one_pow]; norm_num⟩

Result:
no goals

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ (↑p ^ k) / 2)
⊢ (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
rw [heven.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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ (↑p ^ k) / 2)
⊢ 1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ ∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n

Tactic:
by_cases heven : Even ((p ^ k : ℕ).totient / 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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ (↑p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ (↑p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ (↑p ^ k) / 2)
⊢ -1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑(-1) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
norm_num

Result:
no goals

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : Even (φ (↑p ^ k) / 2)
⊢ 1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
norm_num

Result:
no goals

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ (↑p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n

Tactic:
exact ⟨-1, (p : ℕ) ^ (k - 1) * ((p - 1) * k - 1), by
  rw [(not_even_iff_odd.1 heven).neg_one_pow]; norm_num⟩

Result:
no goals

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ ∃ u n, discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑↑p ^ n

Tactic:
rw [discr_prime_pow hζ hirr]

Result:
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ ∃ u n, (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑u * ↑↑p ^ n

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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ (↑p ^ k) / 2)
⊢ (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) =
    ↑↑(-1) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
rw [(not_even_iff_odd.1 heven).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} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
heven : ¬Even (φ (↑p ^ k) / 2)
⊢ -1 * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)) = ↑↑(-1) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))