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

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ p ^ (0 + 1) ≠ 2

Tactic:
simp [hodd]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p ^ (0 + 1)} K L

Tactic:
rw [zero_add, pow_one]

Result:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p} K L

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Tactic:
convert discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2

Result:
case h.e'_3.h.e'_5
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ (-1) ^ ((↑p - 1) / 2) = (-1) ^ (φ (↑p ^ (0 + 1)) / 2)

case h.e'_3.h.e'_6
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ ↑↑p ^ (↑p - 2) = ↑↑p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1))

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ Irreducible (cyclotomic ↑(p ^ (0 + 1)) ?m.190526)

Tactic:
simpa [hirr]

Result:
no goals

Proof state:
case h.e'_3.h.e'_5
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ (-1) ^ ((↑p - 1) / 2) = (-1) ^ (φ (↑p ^ (0 + 1)) / 2)

Tactic:
rw [zero_add, pow_one, totient_prime hp.out]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p} K L

Tactic:
infer_instance

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ IsPrimitiveRoot ζ ↑(p ^ (0 + 1))

Tactic:
simpa using hζ

Result:
no goals

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

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} K L := by
  rw [zero_add, pow_one]
  infer_instance

Result:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Proof state:
case h.e'_3.h.e'_6
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ ↑↑p ^ (↑p - 2) = ↑↑p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1))

Tactic:
rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Tactic:
have hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1):) := by simpa using hζ

Result:
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)