awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
have rw : Odd (2 * (p ^ k * a) - 1)
Tactic: rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos,
        Nat.mul_div_cancel_left _ two_pos, mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow,
        pow_mul, hpo.pow.neg_one_pow]
-- 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
a : ℕ
ha : p - 1 = 2 * a
⊢ Odd (2 * (p ^ k * a) - 1)
have refine : 1 ≤ 2 * (p ^ k * a)
Tactic: refine Nat.Even.sub_odd ?_ (even_two_mul _) odd_one
-- 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
a : ℕ
ha : p - 1 = 2 * a
⊢ 1 ≤ 2 * (p ^ k * a)
have rw : 1 ≤ p ^ k * (p - 1)
Tactic: rw [mul_left_comm, ← ha]
-- 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
⊢ (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))
have H : Eq (α := K[X])
  ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K * (HPow.hPow (α := K[X]) X (p ^ k) - 1)) : K[X])
  ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X (p ^ (k + 1)) - 1) : K[X])
Tactic: have H := congr_arg (@derivative K _) (cyclotomic_prime_pow_mul_X_pow_sub_one K p 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
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 :
  Eq (α := K[X])
    ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K * (HPow.hPow (α := K[X]) X (p ^ k) - 1)) : K[X])
    ((derivative : (a : K[X]) → K[X]) (HPow.hPow (α := K[X]) X (p ^ (k + 1)) - 1) : K[X])
⊢ (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))
have H₁ : HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) (HPow.hPow (α := K[X]) X (p ^ k) - 1) +
    minpoly K ζ * ((↑(p ^ k) : K[X]) * HPow.hPow (α := K[X]) X (p ^ k - 1)) =
  (↑(p ^ (k + 1)) : K[X]) * HPow.hPow (α := K[X]) X (p ^ (k + 1) - 1)
Tactic: rw [derivative_mul, derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_natCast,
      derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_natCast,
      hζ.minpoly_eq_cyclotomic_of_irreducible hirr] at H
Cleared hypotheses: H
-- 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[X]) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) (HPow.hPow (α := K[X]) X (p ^ k) - 1) +
      minpoly K ζ * ((↑(p ^ k) : K[X]) * HPow.hPow (α := K[X]) X (p ^ k - 1)) =
    (↑(p ^ (k + 1)) : K[X]) * HPow.hPow (α := K[X]) X (p ^ (k + 1) - 1)
⊢ (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))
have H₁ : Eq.{v + 1} (α := L)
  ((fun (P : K[X]) ↦ ((aeval ζ : (a : K[X]) → L) P : L))
    (HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X])
        (HPow.hPow (α := K[X]) X (p ^ k) - 1) +
      minpoly K ζ * ((↑(p ^ k) : K[X]) * HPow.hPow (α := K[X]) X (p ^ k - 1))))
  ((fun (P : K[X]) ↦ ((aeval ζ : (a : K[X]) → L) P : L))
    ((↑(p ^ (k + 1)) : K[X]) * HPow.hPow (α := K[X]) X (p ^ (k + 1) - 1)))
Tactic: replace H := congr_arg (fun P => aeval ζ P) H
Cleared hypotheses: H
-- 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 :
  Eq.{v + 1} (α := L)
    ((fun (P : K[X]) ↦ ((aeval ζ : (a : K[X]) → L) P : L))
      (HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X])
          (HPow.hPow (α := K[X]) X (p ^ k) - 1) +
        minpoly K ζ * ((↑(p ^ k) : K[X]) * HPow.hPow (α := K[X]) X (p ^ k - 1))))
    ((fun (P : K[X]) ↦ ((aeval ζ : (a : K[X]) → L) P : L))
      ((↑(p ^ (k + 1)) : K[X]) * HPow.hPow (α := K[X]) X (p ^ (k + 1) - 1)))
⊢ (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))
have H₁ : HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
    (ζ ^ p ^ k - 1) =
  (↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)
Tactic: simp only [aeval_add, aeval_mul, minpoly.aeval, zero_mul, add_zero, aeval_natCast,
      map_sub, aeval_one, aeval_X_pow] at H
Cleared hypotheses: H
-- 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 (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
      (ζ ^ p ^ k - 1) =
    (↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)
⊢ (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))
have H₁ : Eq.{u + 1} (α := K)
  ((Algebra.norm K : (a : L) → K)
      (HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
        (ζ ^ p ^ k - 1)) :
    K)
  ((Algebra.norm K : (a : L) → K) ((↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)) : K)
Tactic: replace H := congr_arg (Algebra.norm K) H
Cleared hypotheses: H
-- 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
H :
  Eq.{u + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
          (ζ ^ p ^ k - 1)) :
      K)
    ((Algebra.norm K : (a : L) → K) ((↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)) : K)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
have pos : ∀ (hp : p = 2), (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
Tactic: by_cases hp : p = 2
-- 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
H :
  Eq.{u + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
          (ζ ^ p ^ k - 1)) :
      K)
    ((Algebra.norm K : (a : L) → K) ((↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)) : K)
pos : ∀ (hp : p = 2), (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
have neg : ∀ (hp : ¬p = 2), (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
Tactic: by_cases hp : p = 2
-- 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 :
  Eq.{u + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
          (ζ ^ p ^ k - 1)) :
      K)
    ((Algebra.norm K : (a : L) → K) ((↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)) : 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) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
Tactic: have hnorm : (norm K) (ζ ^ p ^ k - 1) = (p : K) ^ p ^ k := by
      by_cases hp : p = 2
      · exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
      · exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp
-- 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 :
  Eq.{u + 1} (α := K)
    ((Algebra.norm K : (a : L) → K)
        (HMul.hMul (α := L) ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L)
          (ζ ^ p ^ k - 1)) :
      K)
    ((Algebra.norm K : (a : L) → K) ((↑(p ^ (k + 1)) : L) * ζ ^ (p ^ (k + 1) - 1)) : K)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ 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) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have H₁ : HMul.hMul (α := K)
    ((Algebra.norm K : (a : L) → K)
        ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K ζ) : K[X]) : L) :
      K)
    (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
  HMul.hMul (β := K) (HPow.hPow (α := K) (↑(p ^ k.succ) : K) (p ^ k * (p - 1)))
    ((Algebra.norm K : (a : L) → K) (ζ ^ (p ^ k.succ - 1)) : K)
Tactic: rw [map_mul, hnorm, map_mul, ← map_natCast (algebraMap K L),
      Algebra.norm_algebraMap, finrank L hirr, ← succ_eq_add_one,
      totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ] at H
Cleared hypotheses: H, hnorm
-- 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]) (minpoly K ζ) : K[X]) : L) :
        K)
      (HPow.hPow (α := K) (↑p : K) (p ^ k)) =
    HMul.hMul (β := K) (HPow.hPow (α := K) (↑(p ^ k.succ) : K) (p ^ k * (p - 1)))
      ((Algebra.norm K : (a : L) → K) (ζ ^ (p ^ k.succ - 1)) : K)
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ 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) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have 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 + 1) * (p - 1)))
Tactic: rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow,
      mul_one, cast_pow, ← pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] at H
Cleared hypotheses: H, hnorm
-- 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 + 1) * (p - 1)))
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ 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) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
have this : 0 < k.succ * (p - 1)
Tactic: have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)
-- 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 + 1) * (p - 1)))
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
⊢ (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))
have 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)
Tactic: rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H
Cleared hypotheses: H, hnorm, 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
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)
⊢ (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))
have e_a : ∀
  (H :
    (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 * (k.succ * (p - 1)).pred)),
  (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: replace H := (mul_left_inj' fun h => ?_).1 H
Cleared hypotheses: H
-- 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
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)
e_a :
  ∀
    (H :
      (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 * (k.succ * (p - 1)).pred)),
    (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))
⊢ (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))
have e_a₁ : ∀ (h : HPow.hPow (α := K) (↑p : K) (p ^ k) = 0), False
Tactic: replace H := (mul_left_inj' fun h => ?_).1 H
-- 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
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
H :
  (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 * (k.succ * (p - 1)).pred)
⊢ (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))
have e_a : HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) =
  HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1) - 1))
Tactic: simp only [H, mul_comm _ (k + 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
hnorm : (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)
this : 0 < k.succ * (p - 1)
H :
  (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 * (k.succ * (p - 1)).pred)
⊢ HPow.hPow (α := K) (↑p : K) (p ^ k * (k.succ * (p - 1)).pred) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((k + 1) * (p - 1) - 1))
have e_a : Eq.{u + 1} (α := K) (↑(p ^ (p ^ k * (k.succ * (p - 1)).pred)) : K) (↑(p ^ (p ^ k * ((k + 1) * (p - 1) - 1))) : K)
Tactic: norm_cast