awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
rw :
  0 + HMul.hMul (α := R[X]) (∏ i ∈ n.properDivisors, cyclotomic i R) (cyclotomic n R) =
      HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) ∧
    degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ cyclotomic n R =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
rw [(div_modByMonic_unique (cyclotomic n R) 0 prod_monic _).1]

Premises used: Polynomial.cyclotomic, Polynomial.div_modByMonic_unique, And.left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
simp :
  HMul.hMul (α := R[X]) (∏ i ∈ n.properDivisors, cyclotomic i R) (cyclotomic n R) =
      HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) ∧
    ⊥ < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ 0 + HMul.hMul (α := R[X]) (∏ i ∈ n.properDivisors, cyclotomic i R) (cyclotomic n R) =
      HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) ∧
    degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
simp only [degree_zero, zero_add]

Premises used: Polynomial.degree_zero, zero_add
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
left :
  HMul.hMul (α := R[X]) (∏ i ∈ n.properDivisors, cyclotomic i R) (cyclotomic n R) =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R)
right : ⊥ < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ HMul.hMul (α := R[X]) (∏ i ∈ n.properDivisors, cyclotomic i R) (cyclotomic n R) =
      HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) ∧
    ⊥ < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
left left₁ :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ HMul.hMul (α := R[X]) (∏ i ∈ n.properDivisors, cyclotomic i R) (cyclotomic n R) =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
rw [mul_comm]

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

Tactic:
rw [bot_lt_iff_ne_bot]

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

Tactic:
Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h_1 : Nontrivial R
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
h : degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R) = ⊥
⊢ False

Tactic:
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n m : ℕ
hpos : 0 < n
hm : m ∣ n
hdiff : m ≠ n
⊢ m ∈ n.properDivisors

Tactic:
replace hm := Nat.mem_properDivisors.2
    ⟨hm, lt_of_le_of_ne (Nat.divisor_le (Nat.mem_divisors.2 ⟨hm, hpos.ne'⟩)) hdiff⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
rw :
  HPow.hPow (α := R[X]) X m - 1 ∣
    (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (HPow.hPow (α := R[X]) X m - 1)
⊢ HPow.hPow (α := R[X]) X m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
rw [← Finset.sdiff_union_of_subset (Nat.divisors_subset_properDivisors (ne_of_lt hpos).symm
    (Nat.mem_properDivisors.1 hm).1 (ne_of_lt (Nat.mem_properDivisors.1 hm).2)),
    Finset.prod_union Finset.sdiff_disjoint,
    prod_cyclotomic_eq_X_pow_sub_one (Nat.pos_of_mem_properDivisors hm)]

Premises used: Nat.pos_of_mem_properDivisors, Polynomial.prod_cyclotomic_eq_X_pow_sub_one, Finset.prod_union, Ne.symm, Finset.sdiff_union_of_subset, And.right, And.left, Nat.divisors_subset_properDivisors, Iff.mp, Nat.mem_properDivisors, Finset.sdiff_disjoint, ne_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
rw rw₁ :
  (HPow.hPow (α := R[X]) X m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R =
    (HPow.hPow (α := R[X]) X m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R
⊢ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (HPow.hPow (α := R[X]) X m - 1) =
    (HPow.hPow (α := R[X]) X m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ HPow.hPow (α := R[X]) X m - 1 ∣
    (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (HPow.hPow (α := R[X]) X m - 1)

Tactic:
exact ⟨∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R, by rw [mul_comm]⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
h :
  ∀ (k : ℕ) (hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K))
    {ζ : K} (hz : IsPrimitiveRoot ζ k), Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
⊢ Eq (α := K[X]) (cyclotomic n K) (cyclotomic' n K)

Tactic:
induction n using Nat.strong_induction_on generalizing ζ with | _ k hk
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
h : ∀ (hzero : k = 0), Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
h₁ : ∀ (hpos : k > 0), Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)

Tactic:
obtain hzero | hpos := k.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hzero : k = 0
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)

Tactic:
simp only [hzero, cyclotomic'_zero, cyclotomic_zero]

Premises used: Polynomial.cyclotomic_zero, Polynomial.cyclotomic'_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
obtain : ∀ (d : ℕ) (hd : k = i * d), Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)
⊢ Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)

Tactic:
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1

Premises used: And.left, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = i * d
⊢ k = d * i

Tactic:
rw [mul_comm] at hd

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = d * i
⊢ Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)

Tactic:
hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)

Premises used: IsPrimitiveRoot.pow, And.right, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = d * i
⊢ Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)

Tactic:
exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)

Premises used: IsPrimitiveRoot.pow, And.right, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ ∀ i ∈ k.properDivisors, Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)

Tactic:
have h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K := by
    intro i hi
    obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
    rw [mul_comm] at hd
    exact hk i (Nat.mem_properDivisors.1 hi).2 (IsPrimitiveRoot.pow hpos hz hd)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K} (hz : IsPrimitiveRoot ζ m), Eq (α := K[X]) (cyclotomic m K) (cyclotomic' m K)
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
h : ∀ i ∈ k.properDivisors, Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)
h₁ : (HPow.hPow (α := K[X]) X k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' k K
h₂ :
  (HPow.hPow (α := K[X]) X k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic i K =
    (HPow.hPow (α := K[X]) X k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic' i K
h₃ h₄ :
  (HPow.hPow (α := K[X]) X k - 1) /ₘ ∏ x ∈ k.properDivisors, cyclotomic' x K =
    (HPow.hPow (α := K[X]) X k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic' i K
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)

Tactic:
rw [@cyclotomic_eq_X_pow_sub_one_div _ _ _ hpos, cyclotomic'_eq_X_pow_sub_one_div hpos hz,
    Finset.prod_congr (refl k.properDivisors) h]

Premises used: Finset.prod_congr, Nat.properDivisors, refl, Polynomial.cyclotomic_eq_X_pow_sub_one_div, Polynomial.cyclotomic'_eq_X_pow_sub_one_div
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
⊢ Nontrivial R

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

Tactic:
⟨fun hcycl => ?_, fun hP => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
refine_1 : ∀ (hcycl : P = cyclotomic n R), P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
refine_2 : ∀ (hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1), P = cyclotomic n R
⊢ P = cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1

Tactic:
refine ⟨fun hcycl => ?_, fun hP => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hcycl : P = cyclotomic n R
refine_1 :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) = HPow.hPow (α := R[X]) X n - 1
refine_1₁ :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) = ∏ i ∈ n.divisors, cyclotomic i R
refine_1₂ :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) =
    ∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R
refine_1₃ refine_1₄ :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1

Tactic:
rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← 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
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
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
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
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
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
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
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
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
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
rw :
  0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1 ∧
    degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ P = cyclotomic n R

Tactic:
rw [@cyclotomic_eq_X_pow_sub_one_div R _ _ hpos, (div_modByMonic_unique P 0 prod_monic _).1]

Premises used: Polynomial.div_modByMonic_unique, And.left, OfNat.ofNat, Polynomial.cyclotomic_eq_X_pow_sub_one_div
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
rwa : (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1
rwa₁ rwa₂ rwa₃ rwa₄ : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1

Tactic:
rwa [zero_add, mul_comm]

Premises used: zero_add, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
refine : degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1 ∧
    degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
refine ⟨by rwa [zero_add, mul_comm], ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
rw : degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R) ≠ ⊥
⊢ degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)

Tactic:
rw [degree_zero, bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot, Polynomial.degree_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h_1 : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
h : degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R) = ⊥
⊢ False

Tactic:
Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h_1 : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
h : degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R) = ⊥
⊢ False

Tactic:
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ Eq (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) (cyclotomic (p ^ (m + 1)) R) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1

Tactic:
have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i)
      (pow_pos hp.pos (m + 1))
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  Eq (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) (cyclotomic (p ^ (m + 1)) R) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
⊢ 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)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1

Tactic:
rw [eq_comm] at this

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  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)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
rw :
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1 ↔
    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
rw₁ rw₂ :
  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 ↔
    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
⊢ 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

Tactic:
rw [this, Nat.prod_properDivisors_prime_pow hp]

Premises used: Nat.prod_properDivisors_prime_pow
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ ∀ (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

Tactic:
have : ∀ m, (cyclotomic (p ^ (m + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) ↔
      ((∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) *
        ∏ x ∈ Finset.range (m + 1), cyclotomic (p ^ x) R) = X ^ p ^ (m + 1) - 1 := by
    intro m
    have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i)
      (pow_pos hp.pos (m + 1))
    rw [eq_comm] at this
    rw [this, Nat.prod_properDivisors_prime_pow hp]
-- 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
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this_1 :
  ∀ (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
this : Fact (Nat.Prime p)
⊢ Eq (α := R[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) R)
    (∑ i ∈ range p, HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 0) ^ i)

Tactic:
simp [cyclotomic_prime]

Premises used: Polynomial.cyclotomic_prime