awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
rw :
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
      (∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
⊢ Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1 + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)

Tactic:
rw [← (eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr ?_]

Premises used: Iff.mpr, Polynomial.eq_cyclotomic_iff, pow_pos, Nat.Prime.pos, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
rw :
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i) *
      HMul.hMul (α := R[X]) (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R)
        (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
⊢ HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
      (∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1

Tactic:
rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]

Premises used: Nat.prod_properDivisors_prime_pow, Finset.prod_range_succ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
⊢ HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
      (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) - 1

Tactic:
rw [this] at n_ih
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih :
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
      (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) - 1
rw : HPow.hPow (α := R[X]) X (p ^ (n_n + 1) * p) = HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1))
⊢ (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i) *
      HMul.hMul (α := R[X]) (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R)
        (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1

Tactic:
rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]

Premises used: sub_left_inj, geom_sum_mul, pow_mul, mul_comm, Finset.sum
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih :
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
      (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) - 1
⊢ HPow.hPow (α := R[X]) X (p ^ (n_n + 1) * p) = HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1))

Tactic:
simp only [pow_add, pow_one]

Premises used: pow_add, pow_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
zero :
  Eq (α := R[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) R)
    (∑ i ∈ range p, HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 0) ^ i)
succ :
  ∀ (n_n : ℕ)
    (n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)),
    Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1 + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
⊢ Eq (α := R[X]) (cyclotomic (p ^ (n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n) ^ i)

Tactic:
induction n with
  | zero => haveI := Fact.mk hp; simp [cyclotomic_prime]
  | succ n_n n_ih =>
    rw [← (eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr ?_]
    rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
    rw [this] at n_ih
    rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]
    simp only [pow_add, pow_one]

Premises used: pow_add, sub_left_inj, geom_sum_mul, pow_mul, Nat.prod_properDivisors_prime_pow, pow_one, mul_comm, Finset.prod_range_succ, Polynomial.cyclotomic_prime, Finset.sum
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
rw :
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ k) ^ i) * (HPow.hPow (α := R[X]) X (p ^ k) - 1) =
    HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₁ : HPow.hPow (α := R[X]) X (p ^ k) ^ p - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₂ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₃ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ k * p) - 1
rw₄ rw₅ : HPow.hPow (α := R[X]) X (p * p ^ k) - 1 = HPow.hPow (α := R[X]) X (p * p ^ k) - 1
⊢ cyclotomic (p ^ (k + 1)) R * (HPow.hPow (α := R[X]) X (p ^ k) - 1) = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1

Tactic:
rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]

Premises used: pow_succ, Polynomial.cyclotomic_prime_pow_eq_geom_sum, geom_sum_mul, pow_mul, mul_comm, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : 1 < n
h : ∀ (n : ℕ) (hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1) (hn : 1 < n), coeff (cyclotomic n R) 0 = 1
⊢ coeff (cyclotomic n R) 0 = 1

Tactic:
induction n using Nat.strong_induction_on with | _ n hi
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
rw : (HSub.hSub (α := R[X]) X 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0 = -1
⊢ Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)

Tactic:
rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2
      (lt_of_lt_of_le one_lt_two hn)), Finset.prod_insert (Finset.notMem_erase 1 _),
      cyclotomic_one R]

Premises used: Iff.mpr, Nat.one_mem_properDivisors_iff_one_lt, Finset.prod_insert, Polynomial.cyclotomic_one, one_lt_two, Finset.notMem_erase, OfNat.ofNat, Finset.insert_erase, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ 1 < j

Tactic:
(Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))

Premises used: Nat.pos_of_mem_properDivisors, Nat.succ_le_of_lt, Ne.le_iff_lt, Ne.symm, Finset.mem_erase, And.right, And.left, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ 1 < j

Tactic:
exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))

Premises used: Nat.pos_of_mem_properDivisors, Nat.succ_le_of_lt, Ne.le_iff_lt, Ne.symm, Finset.mem_erase, And.right, And.left, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j

Tactic:
have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
      intro j hj
      apply Nat.succ_le_of_lt
      exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ coeff (cyclotomic j R) 0 = 1

Tactic:
hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)

Premises used: Finset.mem_erase, And.right, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ coeff (cyclotomic j R) 0 = 1

Tactic:
exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)

Premises used: Finset.mem_erase, And.right, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
⊢ ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1

Tactic:
have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 := by
      intro j hj
      exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
rw : Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, 1) 1
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0) 1

Tactic:
rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]

Premises used: Finset.prod_congr, Nat.properDivisors, OfNat.ofNat, Finset.erase, refl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, 1) 1

Tactic:
simp only [Finset.prod_const_one]

Premises used: Finset.prod_const_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0) 1

Tactic:
have hrw : (∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 := by
      rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
      simp only [Finset.prod_const_one]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
hrw : Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0) 1
⊢ (HSub.hSub (α := R[X]) X 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0 = -1

Tactic:
simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]

Premises used: Polynomial.coeff_X_zero, Polynomial.coeff_sub, mul_one, Polynomial.coeff_one_zero, zero_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)

Tactic:
have hprod : (∏ i ∈ Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 := by
    rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2
      (lt_of_lt_of_le one_lt_two hn)), Finset.prod_insert (Finset.notMem_erase 1 _),
      cyclotomic_one R]
    have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
      intro j hj
      apply Nat.succ_le_of_lt
      exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
    have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 := by
      intro j hj
      exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
    have hrw : (∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 := by
      rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
      simp only [Finset.prod_const_one]
    simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₂ :
  (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
rw₃ : coeff (cyclotomic n R) 0 * coeff (∏ x ∈ n.properDivisors, cyclotomic x R) 0 = -coeff (cyclotomic n R) 0
rw₄ : coeff (cyclotomic n R) 0 * ∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₅ : coeff (cyclotomic n R) 0 * -1 = -coeff (cyclotomic n R) 0
rw₆ : -(coeff (cyclotomic n R) 0 * 1) = -coeff (cyclotomic n R) 0
rw₇ rw₈ : -coeff (cyclotomic n R) 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]

Premises used: Polynomial.prod_cyclotomic_eq_X_pow_sub_one, Polynomial.coeff_zero_prod, zero_le_one, Nat.cons_self_properDivisors, Finset.prod_cons, Polynomial.mul_coeff_zero, mul_one, LE.le.trans_lt, LT.lt.ne_bot, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0

Tactic:
have heq : (X ^ n - 1 : R[X]).coeff 0 = -(cyclotomic n R).coeff 0 := by
    rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
rw : eval 0 (HPow.hPow (α := R[X]) X n - 1) = -1
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1

Tactic:
rw [coeff_zero_eq_eval_zero _]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
⊢ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
⊢ eval 0 (HPow.hPow (α := R[X]) X n - 1) = -1

Tactic:
simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_sub]

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_one, Polynomial.eval_sub, zero_pow, zero_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1

Tactic:
have hzero : (X ^ n - 1 : R[X]).coeff 0 = (-1 : R) := by
    rw [coeff_zero_eq_eval_zero _]
    simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_sub]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
hzero : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
⊢ -1 = -coeff (cyclotomic n R) 0

Tactic:
rw [hzero] at heq
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
hzero : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
heq₁ : -1 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1

Tactic:
rw [hzero] at heq
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : -1 = -coeff (cyclotomic n R) 0
hzero : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
⊢ coeff (cyclotomic n R) 0 = 1

Tactic:
neg_inj.mp (Eq.symm heq)

Premises used: neg_inj, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : -1 = -coeff (cyclotomic n R) 0
hzero : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
⊢ coeff (cyclotomic n R) 0 = 1

Tactic:
exact neg_inj.mp (Eq.symm heq)

Premises used: neg_inj, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : 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)
a₁ : p.Coprime a
⊢ a.Coprime p

Tactic:
apply Nat.Coprime.symm

Premises used: Nat.Coprime.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : 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)
a₁ : ¬p ∣ a
⊢ p.Coprime a

Tactic:
rw [hprime.1.coprime_iff_not_dvd]

Premises used: Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : 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 : p ∣ a
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0

Tactic:
replace h := (ZMod.natCast_eq_zero_iff a p).2 h
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : 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) (↑a : ZMod p) 0
⊢ Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0

Tactic:
rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.IsRoot.def, eq_natCast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : 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) (↑a : ZMod p) 0
hroot₁ : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
⊢ Eq (α := ZMod p) (↑a : ZMod p) 0

Tactic:
rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.IsRoot.def, eq_natCast
-- 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
pos : ∀ (hone : n = 1), False
neg : ∀ (hone : ¬n = 1), False
⊢ False

Tactic:
by_cases hone : n = 1
-- 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
⊢ False

Tactic:
simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero,
      one_ne_zero, coeff_sub] at hroot

Premises used: neg_eq_zero, Polynomial.coeff_X_zero, Polynomial.cyclotomic_one, Polynomial.coeff_sub, one_ne_zero, Polynomial.coeff_one_zero, zero_sub
-- 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
⊢ Eq (α := ZMod p) 1 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