awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
hn : n > 0
inr : Dvd.dvd (α := ℤ[X]) (cyclotomic n ℤ) (∏ i ∈ n.divisors, cyclotomic i ℤ)
⊢ cyclotomic n ℤ ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one hn]

Premises used: Polynomial.prod_cyclotomic_eq_X_pow_sub_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
hn : n > 0
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic n ℤ) (∏ i ∈ n.divisors, cyclotomic i ℤ)

Tactic:
Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')

Premises used: Finset.dvd_prod_of_mem, LT.lt.ne', Nat.mem_divisors_self
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : Ring R
hn : n > 0
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic n ℤ) (∏ i ∈ n.divisors, cyclotomic i ℤ)

Tactic:
exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')

Premises used: Finset.dvd_prod_of_mem, LT.lt.ne', Nat.mem_divisors_self
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
this : Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
      Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this

Premises used: Polynomial.map_pow, Polynomial.map_X, congr_arg, Polynomial.map_prod, Int.castRingHom, Polynomial.map_cyclotomic_int, Polynomial.map_sum, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
suffices : Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
suffices (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ Finset.range n, X ^ i by
    simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
      Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
h : 0 < n
R : Type u_1
inst : CommRing R
rw :
  HMul.hMul (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (cyclotomic 1 ℤ) =
    HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₁ :
  ∏ x ∈ n.divisors, cyclotomic x ℤ = HMul.hMul (α := ℤ[X]) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) (cyclotomic 1 ℤ)
rw₂ : ∏ x ∈ n.divisors, cyclotomic x ℤ = (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i) * HSub.hSub (α := ℤ[X]) X 1
rw₃ : ∏ x ∈ n.divisors, cyclotomic x ℤ = HPow.hPow (α := ℤ[X]) X n - 1
rw₄ rw₅ : HPow.hPow (α := ℤ[X]) X n - 1 = HPow.hPow (α := ℤ[X]) X n - 1
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)

Tactic:
rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]

Premises used: Iff.mpr, Finset.prod_erase_mul, Polynomial.cyclotomic_ne_zero, Polynomial.prod_cyclotomic_eq_X_pow_sub_one, Nat.one_mem_divisors, Int, geom_sum_mul, LT.lt.ne', Polynomial.cyclotomic_one, mul_left_inj', OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
this : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
⊢ Eq (α := R[X]) (cyclotomic p R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X i)

Tactic:
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      congr_arg (map (Int.castRingHom R)) this

Premises used: Polynomial.map_pow, Polynomial.map_X, congr_arg, Int.castRingHom, Polynomial.map_cyclotomic_int, Polynomial.map_sum, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
suffices : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)
⊢ Eq (α := R[X]) (cyclotomic p R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X i)

Tactic:
suffices cyclotomic p ℤ = ∑ i ∈ range p, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      congr_arg (map (Int.castRingHom R)) this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ p.divisors.erase 1, cyclotomic i ℤ)
rw₁ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ Finset.erase {1, p} 1, cyclotomic i ℤ)
rw₂ : Eq (α := ℤ[X]) (cyclotomic p ℤ) (∏ i ∈ {p}, cyclotomic i ℤ)
rw₃ rw₄ : cyclotomic p ℤ = cyclotomic p ℤ
⊢ Eq (α := ℤ[X]) (cyclotomic p ℤ) (∑ i ∈ range p, HPow.hPow (α := ℤ[X]) X i)

Tactic:
rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
    erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]

Premises used: Iff.mpr, Finset.mem_singleton, Finset.prod_singleton, Iff.not, Nat.Prime.pos, Ne.symm, Finset.erase_insert, Nat.Prime.ne_one, Polynomial.prod_cyclotomic_eq_geom_sum, Nat.Prime.divisors, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
rw : (∑ i ∈ range p, HPow.hPow (α := R[X]) X i) * HSub.hSub (α := R[X]) X 1 = HPow.hPow (α := R[X]) X p - 1
rw₁ rw₂ : HPow.hPow (α := R[X]) X p - 1 = HPow.hPow (α := R[X]) X p - 1
⊢ cyclotomic p R * HSub.hSub (α := R[X]) X 1 = HPow.hPow (α := R[X]) X p - 1

Tactic:
rw [cyclotomic_prime, geom_sum_mul]

Premises used: geom_sum_mul, Polynomial.cyclotomic_prime
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 2 R = HAdd.hAdd (α := R[X]) X 1

Tactic:
simp [cyclotomic_prime]

Premises used: Polynomial.cyclotomic_prime
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 3 R = HPow.hPow (α := R[X]) (β := ℕ) X 2 + X + 1

Tactic:
simp [cyclotomic_prime, sum_range_succ']

Premises used: Polynomial.cyclotomic_prime, Finset.sum_range_succ'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
this : Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ Dvd.dvd (α := R[X]) (cyclotomic d R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      map_dvd (Int.castRingHom R) this

Premises used: Polynomial.map_dvd, Polynomial.map_pow, Polynomial.map_X, Int.castRingHom, Polynomial.map_cyclotomic_int, Polynomial.map_sum
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
suffices : Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ Dvd.dvd (α := R[X]) (cyclotomic d R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
suffices cyclotomic d ℤ ∣ ∑ i ∈ Finset.range n, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      map_dvd (Int.castRingHom R) this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
inl : ∀ (hdn : d ∣ 0), Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range 0, HPow.hPow (α := ℤ[X]) X i)
inr : ∀ (hn : n > 0), Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d : ℕ
hd : d ≠ 1
hdn : d ∣ 0
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range 0, HPow.hPow (α := ℤ[X]) X i)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
inr : Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)

Tactic:
rw [← prod_cyclotomic_eq_geom_sum hn]

Premises used: Polynomial.prod_cyclotomic_eq_geom_sum
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
inr : d ∈ n.divisors.erase 1
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic d ℤ) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)

Tactic:
apply Finset.dvd_prod_of_mem

Premises used: Finset.dvd_prod_of_mem
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ n.divisors.erase 1

Tactic:
simp [hd, hdn, hn.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ 0 < n

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ 0 < d

Tactic:
have h0d : 0 < d := Nat.pos_of_dvd_of_pos hdvd (by positivity)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
⊢ 0 < n

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
hzero : n ≠ 0
⊢ d.divisors ⊆ n.divisors

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
rw :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    HPow.hPow (α := R[X]) X n - 1
rw₁ :
  HMul.hMul (α := R[X]) (∏ i ∈ d.divisors, cyclotomic i R) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) =
    ∏ i ∈ n.divisors, cyclotomic i R
rw₂ :
  HMul.hMul (α := R[X]) (∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) (∏ i ∈ d.divisors, cyclotomic i R) =
    ∏ i ∈ n.divisors, cyclotomic i R
rw₃ rw₄ : Eq.{u_1 + 1} (α := R[X]) (∏ x ∈ n.divisors, cyclotomic x R) (∏ i ∈ n.divisors, cyclotomic i R)
⊢ (HPow.hPow (α := R[X]) X d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = HPow.hPow (α := R[X]) X n - 1

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one h0d,
    ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]

Premises used: Polynomial.prod_cyclotomic_eq_X_pow_sub_one, Finset.prod_sdiff, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
⊢ d ∣ n ∧ d < n

Tactic:
rw [Nat.mem_properDivisors] at h

Premises used: Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
h₁ :
  HPow.hPow (α := R[X]) X n - 1 =
    (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
⊢ (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R ∣ HPow.hPow (α := R[X]) X n - 1

Tactic:
use ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Premises used: Nat.properDivisors, Nat.divisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
h₁ : n ∉ n.properDivisors \ d.divisors
h₂ : n ∉ d.divisors
h₃ : n ≠ 0
⊢ HPow.hPow (α := R[X]) X n - 1 =
    (HPow.hPow (α := R[X]) X d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Tactic:
rw [← X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h.1 h.2.ne_bot,
    ← Nat.insert_self_properDivisors, Finset.insert_sdiff_of_notMem,
    Finset.prod_insert, mul_assoc]

Premises used: Finset.prod_insert, mul_assoc, Finset.insert_sdiff_of_notMem, Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, And.right, And.left, Nat.insert_self_properDivisors, LT.lt.ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ n.properDivisors \ d.divisors

Tactic:
Finset.notMem_sdiff_of_notMem_left Nat.self_notMem_properDivisors

Premises used: Finset.notMem_sdiff_of_notMem_left, Nat.self_notMem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ n.properDivisors \ d.divisors

Tactic:
exact Finset.notMem_sdiff_of_notMem_left Nat.self_notMem_properDivisors

Premises used: Finset.notMem_sdiff_of_notMem_left, Nat.self_notMem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

Tactic:
fun hk => h.2.not_ge <| Nat.divisor_le hk

Premises used: And.right, LT.lt.not_ge, Nat.divisor_le, Not
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

Tactic:
exact fun hk => h.2.not_ge <| Nat.divisor_le hk

Premises used: And.right, LT.lt.not_ge, Nat.divisor_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0

Tactic:
h.2.ne_bot

Premises used: And.right, LT.lt.ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0

Tactic:
exact h.2.ne_bot

Premises used: And.right, LT.lt.ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inl :
  Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic 0 R) : RatFunc R)
    (∏ i ∈ Nat.divisorsAntidiagonal 0,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
inr :
  ∀ (hpos : n > 0),
    Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
      (∏ i ∈ n.divisorsAntidiagonal,
          HPow.hPow (α := RatFunc R) (β := ℤ)
            ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
            ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
        RatFunc R)
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic 0 R) : RatFunc R)
    (∏ i ∈ Nat.divisorsAntidiagonal 0,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n_1 > 0
n : ℕ
hn : 0 < n
rw :
  Eq.{u_1 + 1} (α := RatFunc R)
    (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R))
    ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (∏ i ∈ n.divisors, cyclotomic i R))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := RatFunc R)
    (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R))
    (∏ x ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic x R))
⊢ Eq (α := RatFunc R)
    (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
    ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]

Premises used: Polynomial.prod_cyclotomic_eq_X_pow_sub_one, map_prod
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
⊢ ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)

Tactic:
have h : ∀ n : ℕ, 0 < n → (∏ i ∈ Nat.divisors n, algebraMap _ (RatFunc R) (cyclotomic i R)) =
      algebraMap _ _ (X ^ n - 1 : R[X]) := by
    intro n hn
    rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
rw :
  ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
      (0 : RatFunc R)
rw₁ :
  ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R)
      ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
      (0 : RatFunc R)
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)

Tactic:
rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos]

Premises used: Iff.mp, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
simp_rw : ∀ (n : ℕ) (hn : 0 < n), ¬Eq (α := R[X]) (cyclotomic n R) 0
⊢ ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
      (0 : RatFunc R)

Tactic:
simp_rw [Ne, IsFractionRing.to_map_eq_zero_iff]

Premises used: IsFractionRing.to_map_eq_zero_iff, Ne
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
simp_rw : ∀ (n : ℕ) (hn : 0 < n), ¬HPow.hPow (α := R[X]) X n - 1 = 0
⊢ ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R)
      ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
      (0 : RatFunc R)

Tactic:
simp_rw [Ne, IsFractionRing.to_map_eq_zero_iff]

Premises used: IsFractionRing.to_map_eq_zero_iff, Ne
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
⊢ ∀ (n : ℕ) (hn : 0 < n), ¬Eq (α := R[X]) (cyclotomic n R) 0

Tactic:
simp [cyclotomic_ne_zero]

Premises used: Polynomial.cyclotomic_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n_1 > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
n : ℕ
hn : 0 < n
hp : (HPow.hPow (α := R[X]) X n - 1).Monic
⊢ ¬HPow.hPow (α := R[X]) X n - 1 = 0

Tactic:
apply Monic.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n_1 > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
n : ℕ
hn : 0 < n
⊢ (HPow.hPow (α := R[X]) X n - 1).Monic

Tactic:
apply monic_X_pow_sub_C _ (ne_of_gt hn)

Premises used: Polynomial.monic_X_pow_sub_C, ne_of_gt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
rw :
  cyclotomic n R =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic i R
⊢ cyclotomic n R = (HPow.hPow (α := R[X]) X n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos, ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons]

Premises used: Polynomial.prod_cyclotomic_eq_X_pow_sub_one, LT.lt.ne', Nat.cons_self_properDivisors, Finset.prod_cons
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
hs : ∀ i ∈ n.properDivisors, Monic (cyclotomic i R)
⊢ Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
apply monic_prod_of_monic

Premises used: Polynomial.monic_prod_of_monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
i : ℕ
hs : i ∈ n.properDivisors → Monic (cyclotomic i R)
⊢ i ∈ n.properDivisors → Monic (cyclotomic i R)

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
i : ℕ
h_1 : i ∈ n.properDivisors
⊢ Monic (cyclotomic i R)

Tactic:
cyclotomic.monic i R

Premises used: Polynomial.cyclotomic.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
i : ℕ
h_1 : i ∈ n.properDivisors
⊢ Monic (cyclotomic i R)

Tactic:
exact cyclotomic.monic i R

Premises used: Polynomial.cyclotomic.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
⊢ Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
have prod_monic : (∏ i ∈ Nat.properDivisors n, cyclotomic i R).Monic := by
    apply monic_prod_of_monic
    intro i _
    exact cyclotomic.monic i R