awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
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)
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))
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k)

Tactic:
cases k
-- 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
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
inst_3 : 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:
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
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)
e_a₁ : HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 n * (2 * (2 * HPow.hPow (α := ℕ) 2 n) - 1)) = 1
⊢ 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:
simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
          ((even_two.mul_right _).mul_right _).neg_one_pow]

Premises used: even_two, Even.mul_right, Even.neg_one_pow, pow_succ'
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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
⊢ Odd p

Tactic:
have hpo : Odd p := hp.out.odd_of_ne_two hp2
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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
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)
⊢ 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

Premises used: Nat.Prime.even_sub_one, Even.two_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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
rw : Odd (2 * (p ^ k * a) - 1)
⊢ HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)

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]

Premises used: Nat.mul_div_cancel_left, mul_assoc, two_pos, mul_left_comm, pow_mul, mul_right_comm, Odd.pow, Odd.mul, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)

Tactic:
Nat.Even.sub_odd ?_ (even_two_mul _) odd_one

Premises used: Nat.Even.sub_odd, even_two_mul, odd_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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
refine : 1 ≤ 2 * (p ^ k * a)
⊢ Odd (2 * (p ^ k * a) - 1)

Tactic:
refine Nat.Even.sub_odd ?_ (even_two_mul _) odd_one

Premises used: Nat.Even.sub_odd, even_two_mul, odd_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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
rw : 1 ≤ p ^ k * (p - 1)
⊢ 1 ≤ 2 * (p ^ k * a)

Tactic:
rw [mul_left_comm, ← ha]

Premises used: mul_left_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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 ≤ p ^ k * (p - 1)

Tactic:
one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt)

Premises used: Iff.mpr, Nat.Prime.one_lt, Nat.Prime.pos, Nat.one_le_pow, one_le_mul, Nat.succ_le_iff, Fact.out, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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 ≤ p ^ k * (p - 1)

Tactic:
exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt)

Premises used: Iff.mpr, Nat.Prime.one_lt, Nat.Prime.pos, Nat.one_le_pow, one_le_mul, Nat.succ_le_iff, Fact.out, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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
⊢ 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)
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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])
⊢ 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

Premises used: Polynomial.derivative_mul, sub_zero, Polynomial.C_eq_natCast, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, Polynomial.derivative_X_pow, Polynomial.derivative_sub, Polynomial.derivative_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)
⊢ 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
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)))
⊢ 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

Premises used: map_sub, Polynomial.aeval_X_pow, Polynomial.aeval_one, MulZeroClass.zero_mul, minpoly.aeval, Polynomial.aeval_mul, add_zero, Polynomial.aeval_natCast, Polynomial.aeval_add
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)
⊢ 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
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)
neg : ∀ (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)

Tactic:
by_cases hp : p = 2
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp_1 : 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)
hp : p = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)

Premises used: le_rfl, congrArg, HSub.hSub, cast, IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero, Nat.cast, HPow.hPow, congrFun', Algebra.norm, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp_1 : 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)
hp : p = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)

Premises used: le_rfl, IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp_1 : 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)
hp : ¬p = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp

Premises used: le_rfl, congrArg, HSub.hSub, cast, IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two, Nat.cast, HPow.hPow, congrFun', Algebra.norm, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp_1 : 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)
hp : ¬p = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ k - 1) = HPow.hPow (α := K) (↑p : K) (p ^ k)

Tactic:
exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp

Premises used: le_rfl, IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)

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
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 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)
⊢ 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

Premises used: Nat.succ_eq_add_one, Algebra.algebraMap, Nat.totient_prime_pow, IsCyclotomicExtension.finrank, map_mul, map_natCast, Nat.pred_succ, Nat.succ_pos, Nat.sub_one, Algebra.norm_algebraMap, Fact.out