awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)
h :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) : ZMod p)
    (0 : ZMod p)
h₁ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic i (ZMod p)) :
      ZMod p)
    (0 : ZMod p)
h₂ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (HMul.hMul (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p))) :
      ZMod p)
    (0 : ZMod p)
h₃ :
  HMul.hMul (α := ZMod p) (β := ZMod p)
      (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
      (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p)) :
        ZMod p) =
    0
h₄ :
  HMul.hMul (α := ZMod p) (β := ZMod p) (0 : ZMod p)
      (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p)) :
        ZMod p) =
    0
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have h₅ : Eq (α := ZMod p) 0 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_3 : ∀
  (this :
    (C : (a : R) → R[X]) r ∣
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p),
  (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
Tactic: have := hpri.dvd_add_pow_sub_pow_of_dvd (C a * X) (-1) (r := C r) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
refine_3 :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_1 : (C : (a : R) → R[X]) r ∣ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X ^ p
Tactic: have := hpri.dvd_add_pow_sub_pow_of_dvd (C a * X) (-1) (r := C r) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
refine_3 :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
refine_1 : (C : (a : R) → R[X]) r ∣ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X ^ p
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_2 : (C : (a : R) → R[X]) r ∣ (↑p : R[X]) * HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X
Tactic: have := hpri.dvd_add_pow_sub_pow_of_dvd (C a * X) (-1) (r := C r) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
this :
  (C : (a : R) → R[X]) r ∣
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_3 : ∀
  (this :
    (C : (a : R) → R[X]) r ∣
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - HPow.hPow (α := R[X]) (-1) p),
  (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
Tactic: rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
this :
  (C : (a : R) → R[X]) r ∣
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p
refine_3 :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - HPow.hPow (α := R[X]) (-1) p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_3₁ : ∀
  (this :
    (C : (a : R) → R[X]) r ∣
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - -HPow.hPow (α := R[X]) 1 p),
  (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
Tactic: rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
this :
  (C : (a : R) → R[X]) r ∣
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p
refine_3 :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - HPow.hPow (α := R[X]) (-1) p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
refine_3₁ :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - -HPow.hPow (α := R[X]) 1 p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_3₂ : ∀ (this : (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - -1),
  (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
Tactic: rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ (↑p : R) * a
this :
  (C : (a : R) → R[X]) r ∣
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + -1) ^ p - HPow.hPow (α := R[X]) (-1) p
refine_3 :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - HPow.hPow (α := R[X]) (-1) p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
refine_3₁ :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - -HPow.hPow (α := R[X]) 1 p),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
refine_3₂ :
  ∀
    (this :
      (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p - -1),
    (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
⊢ (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
have refine_3₃ : ∀ (this : (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1),
  (C : (a : R) → R[X]) r ∣ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X - 1) ^ p + 1
Tactic: rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
have pos : ∀ (hy : y = 0), x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
pos : ∀ (hy : y = 0), x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
have neg : ∀ (hy : ¬y = 0), x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
have pos : x ^ n = x ^ card.{u_2} (α := K) (nthRootsFinset n 1)
Tactic: simp only [hy, zero_pow (Nat.ne_zero_of_lt hpos), sub_zero, mul_zero, prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n = x ^ card.{u_2} (α := K) (nthRootsFinset n 1)
have pos : n = card.{u_2} (α := K) (nthRootsFinset n 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ n = card.{u_2} (α := K) (nthRootsFinset n 1)
have pos : n = n
Tactic: rw [h.card_nthRootsFinset]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
have h₁ : x ^ n - y ^ n = eval (x / y) (HPow.hPow (α := K[X]) X n - 1) * y ^ card.{u_2} (α := K) (nthRootsFinset n 1)
Tactic: convert!
    congr_arg (eval (x / y) · * y ^ card (nthRootsFinset n (1 : K))) <|
      X_pow_sub_one_eq_prod hpos h using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
h₁ : x ^ n - y ^ n = eval (x / y) (HPow.hPow (α := K[X]) X n - 1) * y ^ card.{u_2} (α := K) (nthRootsFinset n 1)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
have h₂ : ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y) =
  eval (x / y) (∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) ζ : K[X])) *
    y ^ card.{u_2} (α := K) (nthRootsFinset n 1)
Tactic: convert!
    congr_arg (eval (x / y) · * y ^ card (nthRootsFinset n (1 : K))) <|
      X_pow_sub_one_eq_prod hpos h using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
have a : Eq (α := K) ((algebraMap R K : (a : R) → K) (x ^ n - y ^ n) : K)
  ((algebraMap R K : (a : R) → K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)) : K)
Tactic: apply FaithfulSMul.algebraMap_injective R K
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) (x ^ n - y ^ n) : K)
    ((algebraMap R K : (a : R) → K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)) : K)
have a : HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) x : K) n -
    HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) y : K) n =
  ∏ x_1 ∈ nthRootsFinset n 1, (algebraMap R K : (a : R) → K) (x - x_1 * y)
Tactic: rw [map_sub, map_pow, map_pow, map_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) x : K) n -
      HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) y : K) n =
    ∏ x_1 ∈ nthRootsFinset n 1, (algebraMap R K : (a : R) → K) (x - x_1 * y)
have a : HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) x : K) n -
    HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) y : K) n =
  ∏ x_1 ∈ nthRootsFinset n 1,
    HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((algebraMap R K : (a : R) → K) y : K))
Tactic: simp_rw [map_sub, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) x : K) n -
      HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) y : K) n =
    ∏ x_1 ∈ nthRootsFinset n 1,
      HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((algebraMap R K : (a : R) → K) y : K))
have h' : IsPrimitiveRoot (M := K) ((algebraMap R K : (a : R) → K) ζ : K) n
Tactic: have h' : IsPrimitiveRoot (algebraMap R K ζ) n :=
    h.map_of_injective <| FaithfulSMul.algebraMap_injective R K
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot (M := K) ((algebraMap R K : (a : R) → K) ζ : K) n
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) x : K) n -
      HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) y : K) n =
    ∏ x_1 ∈ nthRootsFinset n 1,
      HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((algebraMap R K : (a : R) → K) y : K))
have a : Eq.{u_1 + 1} (α := K)
  (∏ ζ ∈ nthRootsFinset n 1,
    HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
      (HMul.hMul (β := K) ζ ((algebraMap R K : (a : R) → K) y : K)))
  (∏ x_1 ∈ nthRootsFinset n 1,
    HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((algebraMap R K : (a : R) → K) y : K)))
Tactic: rw [h'.pow_sub_pow_eq_prod_sub_mul_field _ _ hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot (M := K) ((algebraMap R K : (a : R) → K) ζ : K) n
⊢ Eq.{u_1 + 1} (α := K)
    (∏ ζ ∈ nthRootsFinset n 1,
      HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
        (HMul.hMul (β := K) ζ ((algebraMap R K : (a : R) → K) y : K)))
    (∏ x_1 ∈ nthRootsFinset n 1,
      HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) x : K)
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((algebraMap R K : (a : R) → K) y : K)))
have a : ∀ (a : K) (ha : a ∈ (↑(nthRootsFinset n 1) : Set K)),
  Membership.mem (γ := Set K) ((⇑(algebraMap R K) : (a : R) → K) '' (↑(nthRootsFinset n 1) : Set R)) a
Tactic: refine (prod_nbij (algebraMap R K) (fun a ha ↦ map_mem_nthRootsFinset_one ha _)
    (fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H) (fun a ha ↦ ?_) (fun _ _ ↦ rfl)).symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot (M := K) ((algebraMap R K : (a : R) → K) ζ : K) n
a : K
ha : a ∈ (↑(nthRootsFinset n 1) : Set K)
⊢ Membership.mem (γ := Set K) ((⇑(algebraMap R K) : (a : R) → K) '' (↑(nthRootsFinset n 1) : Set R)) a
have this : ∀ b ∈ (↑(nthRootsFinset n 1) : Set K),
  ∃ (a : R) (_ : a ∈ (↑(nthRootsFinset n 1) : Set R)), b = (algebraMap R K : (a : R) → K) a
Tactic: have := Set.surj_on_of_inj_on_of_ncard_le (s := nthRootsFinset n (1 : R))
    (t := nthRootsFinset n (1 : K)) _ (fun _ hr ↦ map_mem_nthRootsFinset_one hr _)
    (fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H)
    (by simp [h.card_nthRootsFinset, h'.card_nthRootsFinset])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot (M := K) ((algebraMap R K : (a : R) → K) ζ : K) n
a : K
ha : a ∈ (↑(nthRootsFinset n 1) : Set K)
this :
  ∀ b ∈ (↑(nthRootsFinset n 1) : Set K),
    ∃ (a : R) (_ : a ∈ (↑(nthRootsFinset n 1) : Set R)), b = (algebraMap R K : (a : R) → K) a
⊢ Membership.mem (γ := Set K) ((⇑(algebraMap R K) : (a : R) → K) '' (↑(nthRootsFinset n 1) : Set R)) a
have a₁ : ∀ (x : R) (hx : x ∈ (↑(nthRootsFinset n 1) : Set R)) (hx1 : a = (algebraMap R K : (a : R) → K) x),
  Membership.mem (γ := Set K) ((⇑(algebraMap R K) : (a : R) → K) '' (↑(nthRootsFinset n 1) : Set R)) a
Tactic: obtain ⟨x, hx, hx1⟩ := this _ ha
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
⊢ 0 < eval (-1) (cyclotomic n R)
have this : NeZero n
Tactic: haveI := NeZero.of_gt hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (-1) (cyclotomic n R)
have rw : 0 < eval (↑(-1) : ℤ) (cyclotomic n ℤ)
Tactic: rw [← map_cyclotomic_int, ← Int.cast_one, ← Int.cast_neg, eval_intCast_map, Int.coe_castRingHom,
    Int.cast_pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
this : 0 < eval (↑(-1) : ℝ) (cyclotomic n ℝ)
⊢ 0 < eval (↑(-1) : ℤ) (cyclotomic n ℤ)
have this₁ : LT.lt (α := ℝ) 0 ((fun (x : ℤ) ↦ ((↑x : ℝ) : ℝ)) (eval (↑(-1) : ℤ) (cyclotomic n ℤ)))
Tactic: rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (↑(-1) : ℤ) (cyclotomic n ℤ)
have suffices : 0 < eval (↑(-1) : ℝ) (cyclotomic n ℝ)
Tactic: suffices 0 < eval (↑(-1 : ℤ)) (cyclotomic n ℝ) by
    rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this
    simpa only [Int.cast_pos] using this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (↑(-1) : ℝ) (cyclotomic n ℝ)
have simp : 0 < eval (-1) (cyclotomic n ℝ)
Tactic: simp only [Int.cast_one, Int.cast_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (-1) (cyclotomic n ℝ)
have h0 : coeff (cyclotomic n ℝ) 0 = 1
Tactic: have h0 := cyclotomic_coeff_zero ℝ hn.le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
h0 : coeff (cyclotomic n ℝ) 0 = 1
⊢ 0 < eval (-1) (cyclotomic n ℝ)
have h0₁ : eval 0 (cyclotomic n ℝ) = 1
Tactic: rw [coeff_zero_eq_eval_zero] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
⊢ 0 < eval (-1) (cyclotomic n ℝ)
have by_contra! : ∀ (hx : eval (-1) (cyclotomic n ℝ) ≤ 0), False
Tactic: by_contra! hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
⊢ False
have this₁ : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
Tactic: have := intermediate_value_univ (-1) 0 (cyclotomic n ℝ).continuous
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
⊢ False
have obtain : ∀ (y : ℝ) (hy : IsRoot (cyclotomic n ℝ) y), False
Tactic: obtain ⟨y, hy : IsRoot _ y⟩ := this (show (0 : ℝ) ∈ Set.Icc _ _ by simpa [h0] using hx)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : IsRoot (cyclotomic n ℝ) y
⊢ False
have hy₁ : IsPrimitiveRoot y n
Tactic: rw [@isRoot_cyclotomic_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : IsPrimitiveRoot y n
⊢ False
have hn₁ : 2 < orderOf y
Tactic: rw [hy.eq_orderOf] at hn
Cleared hypotheses: hn, hy
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ 0 < eval x (cyclotomic n R)
have h : ∀ (n : ℕ) (ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)) (hn : 2 < n), 0 < eval x (cyclotomic n R)
Tactic: induction n using Nat.strong_induction_on with | _ n ih
Cleared hypotheses: n, hn