awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
⊢ ζ = 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
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
⊢ ζ = 1

Tactic:
have hζone : ζ = 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
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
hζone : ζ = 1
zero :
  Matrix.det (n := Fin 1)
      ((Matrix.of : (a : Fin 1 → Fin 1 → K) → Matrix (Fin 1) (Fin 1) K) fun (i j : Fin 1) ↦
        (((traceForm K L : (a : L) → L →ₗ[K] K) (HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) 1 : L) (↑i : ℕ)) :
              L →ₗ[K] K) :
            (a : L) → K)
          (HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) 1 : L) (↑j : ℕ))) =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)
⊢ Matrix.det (n := Fin (dim (IsPrimitiveRoot.powerBasis K hζ)))
      ((Matrix.of :
          (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim → Fin (IsPrimitiveRoot.powerBasis K hζ).dim → K) →
            Matrix (Fin (IsPrimitiveRoot.powerBasis K hζ).dim) (Fin (IsPrimitiveRoot.powerBasis K hζ).dim) K)
        fun (i j : Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) ↦
        (((traceForm K L : (a : L) → L →ₗ[K] K) (ζ ^ (↑i : ℕ)) : L →ₗ[K] K) : (a : L) → K) (ζ ^ (↑j : ℕ))) =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)

Tactic:
rw [hζ.powerBasis_dim _, hζone, ← (algebraMap K L).map_one,
      minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]

Premises used: Algebra.algebraMap, IsPrimitiveRoot.powerBasis_dim, RingHom.map_one, minpoly.eq_X_sub_C_of_algebraMap_inj, Polynomial.natDegree_X_sub_C, RingHom.injective
-- 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)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
hζone : ζ = 1
zero :
  (Matrix.of : (a : Fin 1 → Fin 1 → K) → Matrix (Fin 1) (Fin 1) K) (fun (i j : Fin 1) ↦ (trace K L : (a : L) → K) 1)
      default default =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)
⊢ Matrix.det (n := Fin 1)
      ((Matrix.of : (a : Fin 1 → Fin 1 → K) → Matrix (Fin 1) (Fin 1) K) fun (i j : Fin 1) ↦
        (((traceForm K L : (a : L) → L →ₗ[K] K) (HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) 1 : L) (↑i : ℕ)) :
              L →ₗ[K] K) :
            (a : L) → K)
          (HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) 1 : L) (↑j : ℕ))) =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)

Tactic:
simp only [map_one, one_pow, Matrix.det_unique, traceForm_apply, mul_one]

Premises used: one_pow, Algebra.traceForm_apply, map_one, mul_one, Matrix.det_unique
-- 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)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
hζone : ζ = 1
zero :
  (Matrix.of : (a : Fin 1 → Fin 1 → K) → Matrix (Fin 1) (Fin 1) K)
      (fun (i j : Fin 1) ↦ HSMul.hSMul (β := K) (φ (HPow.hPow (β := ℕ) p 0)) 1) default default =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)
⊢ (Matrix.of : (a : Fin 1 → Fin 1 → K) → Matrix (Fin 1) (Fin 1) K) (fun (i j : Fin 1) ↦ (trace K L : (a : L) → K) 1)
      default default =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)

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:
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)
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) K)
hζone : ζ = 1
⊢ (Matrix.of : (a : Fin 1 → Fin 1 → K) → Matrix (Fin 1) (Fin 1) K)
      (fun (i j : Fin 1) ↦ HSMul.hSMul (β := K) (φ (HPow.hPow (β := ℕ) p 0)) 1) default default =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 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)
pos :
  ∀ (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))
neg :
  ∀ (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))
⊢ 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:
by_cases hk : p ^ (k + 1) = 2

Premises used: HAdd.hAdd, OfNat.ofNat
-- 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
⊢ p ^ (k + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1

Tactic:
rw [← pow_one 2] at hk

Premises used: pow_one, OfNat.ofNat
-- 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) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
⊢ p = 2

Tactic:
eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk

Premises used: Nat.prime_iff, eq_of_prime_pow_eq, Nat.prime_two, Nat.succ_pos, Iff.mp, Fact.out
-- 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) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
⊢ p = 2

Tactic:
exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk

Premises used: Nat.prime_iff, eq_of_prime_pow_eq, Nat.prime_two, Nat.succ_pos, Iff.mp, Fact.out
-- 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
pos :
  ∀ [hp : Fact (Nat.Prime 2)] [hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1)))
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K))
    (hk : HPow.hPow (α := ℕ) 2 (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) (φ (HPow.hPow (α := ℕ) 2 (k + 1)) / 2) *
        HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 (k + 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * (k + 1) - 1))
⊢ 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:
obtain rfl : p = 2 := by
        rw [← pow_one 2] at hk
        exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk

Premises used: rfl
-- 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
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k + 1) = 2
⊢ HPow.hPow (α := ℕ) 2 (k + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1

Tactic:
nth_rw 2 [← pow_one 2] at hk

Premises used: pow_one, OfNat.ofNat
-- 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
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
⊢ k + 1 = 1

Tactic:
replace hk := Nat.pow_right_injective rfl.le hk
-- 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
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hk : k + 1 = 1
⊢ k = 0

Tactic:
rw [add_eq_right] at hk

Premises used: add_eq_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
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hk : k = 0
pos :
  ∀ [hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)))
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)),
    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) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
        HPow.hPow (α := K) (↑2 : K)
          (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
⊢ 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) (φ (HPow.hPow (α := ℕ) 2 (k + 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 (k + 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * (k + 1) - 1))

Tactic:
subst hk
-- 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 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
pos :
  ∀ (hcycl_1 : IsCyclotomicExtension {2} K L) (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)))
    (hζ_1 : IsPrimitiveRoot ζ 2)
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)),
    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) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
        HPow.hPow (α := K) (↑2 : K)
          (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
⊢ 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) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))

Tactic:
rw [pow_one] at hζ hcycl

Premises used: pow_one
-- 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)
⊢ Eq.{v + 1} (α := L) (-1 : L) ((algebraMap K L : (a : K) → L) (-1) : L)

Tactic:
simp
-- 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)
rw : (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))).natDegree = 1
⊢ natDegree (minpoly K ζ) = 1

Tactic:
rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
          minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]

Premises used: minpoly.eq_X_sub_C_of_algebraMap_inj, FaithfulSMul.algebraMap_injective, 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)
⊢ (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))).natDegree = 1

Tactic:
natDegree_X_sub_C (-1)

Premises used: Polynomial.natDegree_X_sub_C, OfNat.ofNat, 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)
⊢ (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))).natDegree = 1

Tactic:
exact natDegree_X_sub_C (-1)

Premises used: Polynomial.natDegree_X_sub_C, OfNat.ofNat, 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)
⊢ natDegree (minpoly K ζ) = 1

Tactic:
have : natDegree (minpoly K ζ) = 1 := by
        rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
          minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]
        exact natDegree_X_sub_C (-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
pos :
  ∀ (e : Fin (natDegree (minpoly K ζ)) ≃ Fin 1),
    discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ_1))) K (B := L)
        (⇑(basis (IsPrimitiveRoot.powerBasis K hζ_1)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ_1).dim) → L) =
      HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
        HPow.hPow (α := K) (↑2 : K)
          (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ_1))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ_1)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ_1).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))

Tactic:
rcases Fin.equiv_iff_eq.2 this with ⟨e⟩

Premises used: Iff.mpr, Fin.equiv_iff_eq
-- 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 (dim (IsPrimitiveRoot.powerBasis K hζ))) ↦ ζ ^ (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (IsPrimitiveRoot.powerBasis K hζ).dim)) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ_1))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ_1)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ_1).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))

Tactic:
rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]

Premises used: PowerBasis.coe_basis, IsPrimitiveRoot.powerBasis_gen, PowerBasis.basis, IsPrimitiveRoot.powerBasis, Algebra.discr_reindex
-- 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 ζ))) ↦ ζ ^ (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (minpoly K ζ).natDegree)) =
    1
⊢ discr.{u, v, 0} (ι := Fin 1) K (B := L)
      ((fun (i : Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) ↦ ζ ^ (↑i : ℕ)) ∘
        (⇑e.symm : (a : Fin 1) → Fin (IsPrimitiveRoot.powerBasis K hζ).dim)) =
    HPow.hPow (α := K) (-1) (φ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) / 2) *
      HPow.hPow (α := K) (↑2 : K)
        (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 - 1) * (HSub.hSub (α := ℕ) 2 1 * HAdd.hAdd (α := ℕ) 0 1 - 1))

Tactic:
simp only [powerBasis_dim,
        zero_add, pow_one, totient_two, reduceDiv, pow_zero, cast_ofNat, tsub_self,
        Nat.add_one_sub_one, mul_one, mul_zero]

Premises used: Nat.cast_ofNat, Nat.add_one_sub_one, IsPrimitiveRoot.powerBasis_dim, tsub_self, zero_add, pow_zero, MulZeroClass.mul_zero, Nat.totient_two, pow_one, Nat.reduceDiv, mul_one
-- 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
⊢ Eq.{v + 1} (α := L) (-1 : L) ((algebraMap K L : (a : K) → L) (-1) : L)

Tactic:
simp