awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
pos :
  discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ ζ ^ (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1

Tactic:
simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]

Premises used: IsPrimitiveRoot.eq_neg_one_of_two_right
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
h :
  discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
pos :
  (discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) =
    1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1

Tactic:
convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _

Premises used: Algebra.algebraMap, HPow.hPow, OfNat.ofNat, DFunLike.coe, Algebra.discr, Neg.neg
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
h :
  Eq.{v + 1} (α := Fin 1 → L)
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
      (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
    fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (natDegree (minpoly K ζ))) ↦
          HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
h :
  ∀ (i : Fin 1),
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
          (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
        i =
      HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)
⊢ Eq.{v + 1} (α := Fin 1 → L)
    ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
      (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
    fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)

Tactic:
ext i
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
h : HPow.hPow (α := L) (-1) (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 1
⊢ ((fun (i : Fin (natDegree (minpoly K ζ))) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree))
      i =
    HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)

Tactic:
simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]

Premises used: map_neg, pow_zero, Fin.val_eq_zero, map_one, Function.comp_apply
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this_1 : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
this : (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 0
⊢ HPow.hPow (α := L) (-1) (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 1

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
h : (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 0
⊢ HPow.hPow (α := L) (-1) (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 1

Tactic:
suffices (e.symm i : ℕ) = 0 by simp [this]
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
h : (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) < 1
⊢ (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) = 0

Tactic:
rw [← Nat.lt_one_iff]

Premises used: Nat.lt_one_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
⊢ (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) < natDegree (minpoly K ζ)

Tactic:
(e.symm i).2

Premises used: Fin.isLt, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
h : 1 = natDegree (minpoly K ζ)
⊢ (↑((e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree) i) : ℕ) < 1

Tactic:
convert! (e.symm i).2

Premises used: Fin.isLt, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
i : Fin 1
h h₁ : Eq (α := ℕ) 1 1
⊢ 1 = natDegree (minpoly K ζ)

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
pos : Eq.{u + 1} (α := K) ((trace K L : (a : L) → K) 1 : K) (1 : K)
⊢ (discr.{u, v, 0} K (B := L) fun (i : Fin 1) ↦ HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (-1) : L) (↑i : ℕ)) =
    1

Tactic:
simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
          _root_.pow_zero, traceForm_apply, mul_one]

Premises used: Algebra.traceMatrix_apply, Algebra.traceForm_apply, pow_zero, Fin.default_eq_zero, mul_one, Matrix.det_unique, Fin.val_zero, Algebra.discr
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
pos : HSMul.hSMul (β := K) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))) 1 = 1
⊢ Eq.{u + 1} (α := K) ((trace K L : (a : L) → K) 1 : K) (1 : K)

Tactic:
rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]

Premises used: Algebra.algebraMap, Algebra.trace_algebraMap, RingHom.map_one, IsCyclotomicExtension.finrank
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl_1 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ_1 : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
this : natDegree (minpoly K ζ) = 1
e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1
⊢ HSMul.hSMul (β := K) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))) 1 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : ¬p ^ (k + 1) = 2
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (p ^ (k + 1)) / 2) *
      HPow.hPow (α := K) (↑p : K) (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
discr_prime_pow_ne_two hζ hirr hk

Premises used: IsCyclotomicExtension.discr_prime_pow_ne_two, Nat.pred
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : ¬p ^ (k + 1) = 2
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (p ^ (k + 1)) / 2) *
      HPow.hPow (α := K) (↑p : K) (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
exact discr_prime_pow_ne_two hζ hirr hk

Premises used: IsCyclotomicExtension.discr_prime_pow_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
rw :
  ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
⊢ ∃ (u : ℤˣ) (n : ℕ),
    discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
        (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n

Tactic:
rw [discr_prime_pow hζ hirr]

Premises used: IsCyclotomicExtension.discr_prime_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
pos :
  ∀ (heven : Even (φ (p ^ k) / 2)),
    ∃ (u : ℤˣ) (n : ℕ),
      HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
        (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
neg :
  ∀ (heven : ¬Even (φ (p ^ k) / 2)),
    ∃ (u : ℤˣ) (n : ℕ),
      HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
        (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n
⊢ ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n

Tactic:
by_cases heven : Even ((p ^ k).totient / 2)

Premises used: HDiv.hDiv, Nat.totient, HPow.hPow, Even, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
rw :
  1 * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑1 : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑1 : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rw [heven.neg_one_pow]

Premises used: Even.neg_one_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ 1 * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑1 : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n

Tactic:
exact ⟨1, p ^ (k - 1) * ((p - 1) * k - 1), by rw [heven.neg_one_pow]; simp⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
rw :
  -1 * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑(-1) : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
⊢ HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑(-1) : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rw [(not_even_iff_odd.1 heven).neg_one_pow]

Premises used: Nat.not_even_iff_odd, Iff.mp, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ -1 * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (↑(↑(-1) : ℤ) : K) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    HPow.hPow (α := K) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1)) =
      (↑(↑u : ℤ) : K) * HPow.hPow (α := K) (↑p : K) n

Tactic:
exact ⟨-1, p ^ (k - 1) * ((p - 1) * k - 1), by
      rw [(not_even_iff_odd.1 heven).neg_one_pow]; simp⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
rw : IsCyclotomicExtension {p} K L
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L

Tactic:
rw [zero_add, pow_one]

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p} K L

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} K L := by
    rw [zero_add, pow_one]
    infer_instance
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simpa using hζ
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
have hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Irreducible (M := K[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) K)

Tactic:
simpa [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ p ^ HAdd.hAdd (α := ℕ) 0 1 ≠ 2

Tactic:
simp [hodd]