awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
refine_1 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))
refine_2 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    minpoly ℚ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) =
      Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)))
refine_3 :
  ∀ (i : Fin (dim (subOnePowerBasis ℚ hζ))) (j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))),
    IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)
have refine_4 : ∀ (i : Fin (dim (subOnePowerBasis ℚ hζ))) (j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))),
  minpoly ℚ (gen (subOnePowerBasis ℚ hζ)) = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (subOnePowerBasis ℚ hζ)))
Tactic: refine discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (subOnePowerBasis ℚ hζ))
j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
⊢ minpoly ℚ (gen (subOnePowerBasis ℚ hζ)) = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (subOnePowerBasis ℚ hζ)))
have refine_4 : IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))
Tactic: refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) ?_
-- 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
⊢ 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 * ((p - 1) * (k + 1) - 1))
have hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
Tactic: haveI hne := IsCyclotomicExtension.neZero' (p ^ (k + 1)) K L
-- 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)
⊢ 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 * ((p - 1) * (k + 1) - 1))
have mf : Module.Finite K L
Tactic: haveI mf : Module.Finite K L := finiteDimensional {p ^ (k + 1)} K L
-- 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
⊢ 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 * ((p - 1) * (k + 1) - 1))
have se : Algebra.IsSeparable K L
Tactic: haveI se : Algebra.IsSeparable K L := isSeparable {p ^ (k + 1)} K L
-- 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
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
⊢ 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 * ((p - 1) * (k + 1) - 1))
have rw : HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2))
    ((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) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
Tactic: rw [discr_powerBasis_eq_norm, finrank L hirr, hζ.powerBasis_gen _,
    ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, totient_prime_pow hp.out (succ_pos k),
    Nat.add_one_sub_one]
-- 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
⊢ HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2))
      ((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) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have hp2 : p = 2 → k ≠ 0
Tactic: have hp2 : p = 2 → k ≠ 0 := by
    rintro rfl rfl
    exact absurd rfl hk
-- 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
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
⊢ HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2))
      ((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) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have e_a : HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
Tactic: congr 1
-- 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
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
e_a :
  HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
⊢ HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2))
      ((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) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have e_a₁ : (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) =
  HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
Tactic: congr 1
-- 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
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
⊢ HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
have e_a : ∀ [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L] [hp : Fact (Nat.Prime 2)]
  (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)
  (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : K)) (hp2 : Eq (α := ℕ) 2 2 → k ≠ 0),
  HPow.hPow (α := K) (-1)
      (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 * (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 - 1) / 2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 / 2)
Tactic: rcases eq_or_ne p 2 with (rfl | hp2)
Cleared hypotheses: p, inst_3, hp, hζ, hirr, hk, hne, hp2
-- 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
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
e_a :
  ∀ [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L] [hp : Fact (Nat.Prime 2)]
    (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) (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : K))
    (hp2 : Eq (α := ℕ) 2 2 → k ≠ 0),
    HPow.hPow (α := K) (-1)
        (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 * (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 - 1) / 2) =
      HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 / 2)
⊢ HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
have e_a₁ : ∀ (hp2 : p ≠ 2),
  HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
Tactic: rcases eq_or_ne p 2 with (rfl | hp2)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hp : Fact (Nat.Prime 2)
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
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k ≠ 0
⊢ HPow.hPow (α := K) (-1)
      (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 * (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 - 1) / 2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 / 2)
have e_a : ∀ (k : ℕ) [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L]
  (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1)))
  (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K))
  (hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2) (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K))
  (hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0),
  HPow.hPow (α := K) (-1)
      (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 *
          (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 - 1) /
        2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 / 2)
Tactic: rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩
Cleared hypotheses: k, inst_3, hζ, hirr, hk, hne, hp2
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
⊢ HPow.hPow (α := K) (-1)
      (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 *
          (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 - 1) /
        2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 / 2)
have e_a : HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * (HPow.hPow (α := ℕ) 2 k.succ - 1) / 2) =
  HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ / 2)
Tactic: rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * (HPow.hPow (α := ℕ) 2 k.succ - 1) / 2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ / 2)
have e_a : HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1) / 2) =
  HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k / 2)
Tactic: simp only [_root_.pow_succ']
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
⊢ HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1) / 2) =
    HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k / 2)
have e_a : HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1)) =
  HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k)
Tactic: rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k)
have e_a : ∀ [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (succ 0 + 1)} K L]
  (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (succ 0 + 1)))
  (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (succ 0 + 1)) K))
  (hk : HPow.hPow (α := ℕ) 2 (succ 0 + 1) ≠ 2) (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (succ 0 + 1)) : K))
  (hp2 : Eq (α := ℕ) 2 2 → succ 0 ≠ 0),
  HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) (β := ℕ) 2 0 * (2 * HPow.hPow (α := ℕ) (β := ℕ) 2 0 - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) (β := ℕ) 2 0)
Tactic: cases k
Cleared hypotheses: k, inst_3, hζ, hirr, hk, hne, hp2
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
e_a :
  ∀ [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (succ 0 + 1)} K L]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (succ 0 + 1)))
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (succ 0 + 1)) K))
    (hk : HPow.hPow (α := ℕ) 2 (succ 0 + 1) ≠ 2) (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (succ 0 + 1)) : K))
    (hp2 : Eq (α := ℕ) 2 2 → succ 0 ≠ 0),
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) (β := ℕ) 2 0 * (2 * HPow.hPow (α := ℕ) (β := ℕ) 2 0 - 1)) =
      HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) (β := ℕ) 2 0)
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k)
have e_a₁ : ∀ (n : ℕ) [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)} K L]
  (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)))
  (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)) K))
  (hk : HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1) ≠ 2)
  (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)) : K))
  (hp2 : Eq (α := ℕ) 2 2 → (n + 1).succ ≠ 0),
  HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 (n + 1) * (2 * HPow.hPow (α := ℕ) 2 (n + 1) - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 (n + 1))
Tactic: cases k
Cleared hypotheses: k, inst_3, hζ, hirr, hk, hne, hp2
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
n : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → (n + 1).succ ≠ 0
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 (n + 1) * (2 * HPow.hPow (α := ℕ) 2 (n + 1) - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 (n + 1))
have e_a : HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 n * (2 * (2 * HPow.hPow (α := ℕ) 2 n) - 1)) =
  HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 n)
Tactic: simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
          ((even_two.mul_right _).mul_right _).neg_one_pow]
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
n : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 ((n + 1).succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → (n + 1).succ ≠ 0
e_a :
  HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 n * (2 * (2 * HPow.hPow (α := ℕ) 2 n) - 1)) =
    HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 n)
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 (n + 1) * (2 * HPow.hPow (α := ℕ) 2 (n + 1) - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 (n + 1))
have e_a₁ : HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 n * (2 * (2 * HPow.hPow (α := ℕ) 2 n) - 1)) = 1
Tactic: simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
          ((even_two.mul_right _).mul_right _).neg_one_pow]
-- 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_1 : p = 2 → k ≠ 0
hp2 : p ≠ 2
⊢ HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
have hpo : Odd p
Tactic: have hpo : Odd p := hp.out.odd_of_ne_two hp2
-- 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
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_1 : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
⊢ HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
have e_a : ∀ (a : ℕ) (ha : p - 1 = 2 * a),
  HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
Tactic: obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd