awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
hone : ¬n = 1
hroot₁ : Eq (α := ZMod p) 1 0
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0

Tactic:
rw [cyclotomic_coeff_zero (ZMod p) (Nat.succ_le_of_lt
    (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at hroot

Premises used: Nat.succ_le_of_lt, Ne.symm, Polynomial.cyclotomic_coeff_zero, ZMod, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
hone : ¬n = 1
hroot₁ : Eq (α := ZMod p) 1 0
h₁ : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ ¬n = 1

Tactic:
rw [cyclotomic_coeff_zero (ZMod p) (Nat.succ_le_of_lt
    (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at hroot

Premises used: Nat.succ_le_of_lt, Ne.symm, Polynomial.cyclotomic_coeff_zero, ZMod, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) 1 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
hone : ¬n = 1
⊢ False

Tactic:
one_ne_zero hroot

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) 1 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
hone : ¬n = 1
⊢ False

Tactic:
exact one_ne_zero hroot

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
h : ZMod.unitOfCoprime a ⋯ ^ n = 1
⊢ orderOf (ZMod.unitOfCoprime a ⋯) ∣ n

Tactic:
apply orderOf_dvd_of_pow_eq_one

Premises used: orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
hpow :
  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)
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) n - 1 = 0

Tactic:
simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_one, Polynomial.eval_sub, eq_natCast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
hpow : HPow.hPow (α := ZMod p) (↑a : ZMod p) n - 1 = 0
apply : (↑(ZMod.unitOfCoprime a ⋯ ^ n) : ZMod p) = 1
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

Tactic:
apply Units.val_eq_one.1

Premises used: Iff.mp, Units.val_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
hpow : HPow.hPow (α := ZMod p) (↑a : ZMod p) n - 1 = 0
⊢ (↑(ZMod.unitOfCoprime a ⋯ ^ n) : ZMod p) = 1

Tactic:
simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]

Premises used: sub_eq_zero, Iff.mp, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
h :
  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)
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

Tactic:
suffices hpow : eval (Nat.castRingHom (ZMod p) a) (X ^ n - 1 : (ZMod p)[X]) = 0 by
    simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow
    apply Units.val_eq_one.1
    simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
⊢ Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)

Tactic:
rw [IsRoot.def] at hroot

Premises used: Polynomial.IsRoot.def
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
h₅ h₆ : Eq (α := ZMod p) 0 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)

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]

Premises used: Polynomial.prod_cyclotomic_eq_X_pow_sub_one, MulZeroClass.zero_mul, Polynomial.eval_mul, ZMod, LT.lt.ne', Nat.cons_self_properDivisors, Finset.prod_cons
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
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
⊢ (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) ?_ ?_
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
refine_3₃ refine_3₄ refine_3₅ 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

Tactic:
rwa [← sub_eq_add_neg, (hpri.odd_of_ne_two hp).neg_pow, one_pow, sub_neg_eq_add] at this

Premises used: one_pow, Odd.neg_pow, sub_eq_add_neg, Nat.Prime.odd_of_ne_two, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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 ^ p

Tactic:
simp only [mul_pow, ← map_pow, dvd_mul_right, (_root_.map_dvd C h₁).trans]

Premises used: Polynomial.C, map_pow, map_dvd, dvd_mul_right, mul_pow, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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 ∣ (↑p : R[X]) * HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X

Tactic:
simp only [map_mul, map_natCast, ← mul_assoc, dvd_mul_right, (_root_.map_dvd C h₂).trans]

Premises used: Polynomial.C, mul_assoc, map_mul, map_dvd, map_natCast, dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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)
neg : ∀ (hy : ¬y = 0), x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
pos : x ^ n = x ^ card.{u_2} (α := K) (nthRootsFinset n 1)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

Tactic:
simp only [hy, zero_pow (Nat.ne_zero_of_lt hpos), sub_zero, mul_zero, prod_const]

Premises used: sub_zero, Finset.prod_const, MulZeroClass.mul_zero, Nat.ne_zero_of_lt, zero_pow
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
pos : n = card.{u_2} (α := K) (nthRootsFinset n 1)
⊢ x ^ n = x ^ card.{u_2} (α := K) (nthRootsFinset n 1)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
pos pos₁ : n = n
⊢ n = card.{u_2} (α := K) (nthRootsFinset n 1)

Tactic:
rw [h.card_nthRootsFinset]

Premises used: IsPrimitiveRoot.card_nthRootsFinset
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ Eq.{u_2 + 1} (α := K)
    ((fun (x_1 : K[X]) ↦ eval (x / y) x_1 * y ^ card.{u_2} (α := K) (nthRootsFinset n 1))
      (HPow.hPow (α := K[X]) X n - 1))
    ((fun (x_1 : K[X]) ↦ eval (x / y) x_1 * y ^ card.{u_2} (α := K) (nthRootsFinset n 1))
      (∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) ζ : K[X])))

Tactic:
congr_arg (eval (x / y) · * y ^ card (nthRootsFinset n (1 : K))) <|
      X_pow_sub_one_eq_prod hpos h

Premises used: Polynomial.eval, HMul.hMul, Polynomial.X_pow_sub_one_eq_prod, HDiv.hDiv, congr_arg, HPow.hPow, Polynomial.nthRootsFinset, Finset.card, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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)
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)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

Tactic:
convert!
    congr_arg (eval (x / y) · * y ^ card (nthRootsFinset n (1 : K))) <|
      X_pow_sub_one_eq_prod hpos h using 1

Premises used: Polynomial.eval, HMul.hMul, Polynomial.X_pow_sub_one_eq_prod, HDiv.hDiv, congr_arg, HPow.hPow, Polynomial.nthRootsFinset, Finset.card, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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 = eval (x / y) (HPow.hPow (α := K[X]) X n - 1) * y ^ card.{u_2} (α := K) (nthRootsFinset n 1)

Tactic:
simp [sub_mul, div_pow, hy, h.card_nthRootsFinset]

Premises used: IsPrimitiveRoot.card_nthRootsFinset, sub_mul, div_pow
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ 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:
simp [eval_prod, prod_mul_pow_card, sub_mul, hy]

Premises used: Polynomial.eval_prod, Finset.prod_mul_pow_card, sub_mul
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
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)
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y)

Tactic:
apply FaithfulSMul.algebraMap_injective R K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
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)
⊢ 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:
rw [map_sub, map_pow, map_pow, map_prod]

Premises used: map_sub, map_pow, map_prod
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
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))
⊢ 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:
simp_rw [map_sub, map_mul]

Premises used: map_sub, map_mul
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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 :
  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)))
⊢ 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:
rw [h'.pow_sub_pow_eq_prod_sub_mul_field _ _ hpos]

Premises used: _private.0.IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul_field
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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)))

Tactic:
(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

Premises used: Algebra.algebraMap, Set.Mem, Polynomial.map_mem_nthRootsFinset_one, setOf, FaithfulSMul.algebraMap_injective, Eq.symm, DFunLike.coe, Finset.prod_nbij, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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 :
  ∀ (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
⊢ 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:
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

Premises used: Algebra.algebraMap, Polynomial.map_mem_nthRootsFinset_one, FaithfulSMul.algebraMap_injective, Eq.symm, DFunLike.coe, Finset.prod_nbij, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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)
⊢ (↑(nthRootsFinset n 1) : Set K).ncard ≤ (↑(nthRootsFinset n 1) : Set R).ncard

Tactic:
simp [h.card_nthRootsFinset, h'.card_nthRootsFinset]

Premises used: IsPrimitiveRoot.card_nthRootsFinset
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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)
⊢ ∀ 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])
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
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
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
⊢ Membership.mem (γ := Set K) ((⇑(algebraMap R K) : (a : R) → K) '' (↑(nthRootsFinset n 1) : Set R)) a

Tactic:
obtain ⟨x, hx, hx1⟩ := this _ ha
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x_1 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
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:
⟨x, hx, hx1.symm⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x_1 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
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:
exact ⟨x, hx, hx1.symm⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
ζ : R
n : ℕ
x y : R
inst_1 : IsDomain R
hodd : Odd n
h : IsPrimitiveRoot ζ n
⊢ x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n 1, (x + ζ * y)

Tactic:
simpa [hodd.neg_pow] using h.pow_sub_pow_eq_prod_sub_mul x (-y) hodd.pos

Premises used: Odd.neg_pow, Odd.pos, IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
⊢ Separable.{u_2} (R := K) (cyclotomic n K)

Tactic:
.of_dvd (separable_X_pow_sub_C 1 NeZero.out one_ne_zero) (cyclotomic.dvd_X_pow_sub_one n K)

Premises used: Polynomial.separable_X_pow_sub_C, Polynomial.cyclotomic.dvd_X_pow_sub_one, NeZero.out, one_ne_zero, OfNat.ofNat, Polynomial.Separable.of_dvd