awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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 + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
⊢ False
have this₁ : Ne.{u + 1} (α := K) (↑(p ^ (k + 1)) : K) 0
Tactic: have := hne.1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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 + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  HMul.hMul (α := K)
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) * HPow.hPow (α := K) (↑p : K) (p ^ k)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this_1 : 0 < k.succ * (p - 1)
h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0
this : Ne.{u + 1} (α := K) (↑(p ^ (k + 1)) : K) 0
⊢ False
have this₁ : ¬Eq.{u + 1} (α := K) (↑p : K) 0
Tactic: rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by lia)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hcycl : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) 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) (φ (p ^ k) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
have zero : ∀ [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)),
  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 (β := ℕ) p 0) / 2) *
      HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 1))
Tactic: rcases k with - | k
Cleared hypotheses: k, hcycl, hζ, hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
hcycl : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ k) K)
zero :
  ∀ [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)),
    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 (β := ℕ) p 0) / 2) *
        HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 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) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ (k - 1) * ((p - 1) * k - 1))
have succ : ∀ (k : ℕ) [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
  (hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 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) (φ (p ^ (k + 1)) / 2) *
      HPow.hPow (α := K) (↑p : K) (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))
Tactic: rcases k with - | k
Cleared hypotheses: k, hcycl, hζ, hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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)
⊢ 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 (β := ℕ) p 0) / 2) *
      HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * ((p - 1) * 0 - 1))
have zero : 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: simp only [coe_basis, _root_.pow_zero, powerBasis_gen _ hζ, totient_one, mul_zero,
      show 1 / 2 = 0 by rfl, discr, traceMatrix]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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)
⊢ 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)
have hζone : ζ = 1
Tactic: have hζone : ζ = 1 := by simpa using hζ
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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.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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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.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)
have 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)
Tactic: simp only [map_one, one_pow, Matrix.det_unique, traceForm_apply, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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) ↦ (trace K L : (a : L) → K) 1)
      default default =
    1 * HPow.hPow (α := K) (↑p : K) (p ^ HSub.hSub (α := ℕ) 0 1 * HSub.hSub (α := ℕ) 0 1)
have 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)
Tactic: rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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)
⊢ 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))
have 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))
Tactic: by_cases hk : p ^ (k + 1) = 2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases hk : p ^ (k + 1) = 2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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 = 2
have hk₁ : p ^ (k + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
Tactic: rw [← pow_one 2] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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))
have 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))
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
Cleared hypotheses: p, hp, hcycl, hζ, hirr, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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
⊢ 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))
have hk₁ : HPow.hPow (α := ℕ) 2 (k + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
Tactic: nth_rw 2 [← pow_one 2] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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
⊢ 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))
have hk₁ : k + 1 = 1
Tactic: replace hk := Nat.pow_right_injective rfl.le hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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
⊢ 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))
have hk₁ : k = 0
Tactic: rw [add_eq_right] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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
⊢ 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))
have 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))
Tactic: subst hk
Cleared hypotheses: k, hcycl, hζ, hirr, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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)
⊢ 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))
have 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))
Tactic: rw [pow_one] at hζ hcycl
Cleared hypotheses: hζ, hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
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
have rw : (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))).natDegree = 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (hypothesis)
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)
⊢ 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))
have this : 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)