awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
by : ⊤ = p.contentIdeal * q.contentIdeal
⊢ ⊤ ≤ (p * q).contentIdeal.radical

Tactic:
calc
    ⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul

Premises used: Polynomial.contentIdeal, HMul.hMul, Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul, Ideal.radical
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
rw : (↑p.coeffs : Set R) ⊆ (↑(span {p.content}) : Set R)
⊢ p.contentIdeal ≤ span {p.content}

Tactic:
rw [contentIdeal_def, span_le]

Premises used: Ideal.span_le, Polynomial.contentIdeal_def
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : R
h1 : a ∈ (↑p.coeffs : Set R)
⊢ ∃ n ∈ p.support, a = p.coeff n

Tactic:
rw [Finset.mem_coe, mem_coeffs_iff] at h1

Premises used: Polynomial.mem_coeffs_iff, Finset.mem_coe
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : R
h1 : ∃ n ∈ p.support, a = p.coeff n
obtain : ∀ n ∈ p.support, ∀ (h2 : a = p.coeff n), a ∈ (↑(span {p.content}) : Set R)
⊢ a ∈ (↑(span {p.content}) : Set R)

Tactic:
obtain ⟨n, _, h2⟩ := h1
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : R
n : ℕ
left : n ∈ p.support
h2 : a = p.coeff n
rw : p.content ∣ p.coeff n
⊢ a ∈ (↑(span {p.content}) : Set R)

Tactic:
rw [SetLike.mem_coe, h2, mem_span_singleton]

Premises used: SetLike.mem_coe, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : R
n : ℕ
left : n ∈ p.support
h2 : a = p.coeff n
⊢ p.content ∣ p.coeff n

Tactic:
content_dvd_coeff n

Premises used: Polynomial.content_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : R
n : ℕ
left : n ∈ p.support
h2 : a = p.coeff n
⊢ p.content ∣ p.coeff n

Tactic:
exact content_dvd_coeff n

Premises used: Polynomial.content_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
apply : span {p.content} ≤ p.contentIdeal
⊢ p.contentIdeal = span {p.content}

Tactic:
apply le_antisymm contentIdeal_le_span_content

Premises used: le_antisymm, Polynomial.contentIdeal_le_span_content
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
rw : ∀ b ∈ p.support, Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff b
⊢ span {p.content} ≤ p.contentIdeal

Tactic:
rw [← p.contentIdeal.span_singleton_generator, span_singleton_le_span_singleton, content,
    Finset.dvd_gcd_iff]

Premises used: Polynomial.contentIdeal, Ideal.span_singleton_le_span_singleton, Ideal.span_singleton_generator, Polynomial.content, Finset.dvd_gcd_iff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ ∀ b ∈ p.support, Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff b

Tactic:
fun n _ ↦ h_prin.contentIdeal_generator_dvd_coeff n

Premises used: Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ ∀ b ∈ p.support, Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff b

Tactic:
exact fun n _ ↦ h_prin.contentIdeal_generator_dvd_coeff n

Premises used: Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
inst_1 : IsBezout R
p : R[X]
⊢ p.IsPrimitive ↔ p.contentIdeal = ⊤

Tactic:
(IsBezout.isPrincipal_of_FG _ p.contentIdeal_FG).isPrimitive_iff_contentIdeal_eq_top

Premises used: Polynomial.contentIdeal_FG, IsBezout.isPrincipal_of_FG, Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq (α := R[X]) (cyclotomic' 0 R) 1

Tactic:
simp only [cyclotomic', Finset.prod_empty, primitiveRoots_zero]

Premises used: Finset.prod_empty, primitiveRoots_zero, Polynomial.cyclotomic'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
⊢ cyclotomic' 1 R = HSub.hSub (α := R[X]) X 1

Tactic:
simp only [cyclotomic', Finset.prod_singleton, map_one, IsPrimitiveRoot.primitiveRoots_one]

Premises used: Finset.prod_singleton, map_one, IsPrimitiveRoot.primitiveRoots_one, Polynomial.cyclotomic'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : CharP R p
hp : p ≠ 2
simp : IsPrimitiveRoot.{u_2} (M := R) (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1
⊢ primitiveRoots 2 R = {-1}

Tactic:
simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]

Premises used: two_pos, Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot.{u_2} (M := R) (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1

Tactic:
⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩

Premises used: And.intro, IsPrimitiveRoot.neg_one, IsPrimitiveRoot.eq_neg_one_of_two_right
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot.{u_2} (M := R) (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1

Tactic:
exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : CharP R p
hp : p ≠ 2
⊢ primitiveRoots 2 R = {-1}

Tactic:
have prim_root_two : primitiveRoots 2 R = {(-1 : R)} := by
    simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
    exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : CharP R p
hp : p ≠ 2
prim_root_two : primitiveRoots 2 R = {-1}
⊢ ∏ μ ∈ primitiveRoots 2 R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) =
    HAdd.hAdd (α := R[X]) X 1

Tactic:
simp only [prim_root_two, Finset.prod_singleton, map_neg, map_one, sub_neg_eq_add]

Premises used: Finset.prod_singleton, map_neg, map_one, sub_neg_eq_add
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
⊢ Monic (cyclotomic' n R)

Tactic:
monic_prod_of_monic _ _ fun _ _ => monic_X_sub_C _

Premises used: Polynomial.monic_X_sub_C, Polynomial.monic_prod_of_monic, Polynomial.cyclotomic'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
⊢ Ne (α := R[X]) (cyclotomic' n R) 0

Tactic:
(cyclotomic'.monic n R).ne_zero

Premises used: Polynomial.cyclotomic'.monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
rw :
  ∑ i ∈ primitiveRoots n R, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).natDegree = n.totient
rw₁ : ∀ i ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ≠ 0
⊢ natDegree (R := R) (∏ μ ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X])) =
    n.totient

Tactic:
rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]

Premises used: Polynomial.C, Polynomial.natDegree_prod, HSub.hSub, primitiveRoots, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i ∈ primitiveRoots n R, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).natDegree = n.totient

Tactic:
simp only [IsPrimitiveRoot.card_primitiveRoots h, mul_one, natDegree_X_sub_C, Nat.cast_id,
      Finset.sum_const, nsmul_eq_mul]

Premises used: Nat.cast_id, Polynomial.natDegree_X_sub_C, IsPrimitiveRoot.card_primitiveRoots, nsmul_eq_mul, mul_one, Finset.sum_const
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
_ : z ∈ primitiveRoots n R → HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) z : R[X]) ≠ 0
⊢ z ∈ primitiveRoots n R → HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) z : R[X]) ≠ 0

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
h_1 : z ∈ primitiveRoots n R
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) z : R[X]) ≠ 0

Tactic:
X_sub_C_ne_zero z

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
h_1 : z ∈ primitiveRoots n R
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) z : R[X]) ≠ 0

Tactic:
exact X_sub_C_ne_zero z

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ degree (cyclotomic' n R) = (↑n.totient : WithBot ℕ)

Tactic:
simp only [degree_eq_natDegree (cyclotomic'_ne_zero n R), natDegree_cyclotomic' h]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_cyclotomic', Polynomial.cyclotomic'_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
⊢ roots (∏ μ ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X])) =
    (primitiveRoots n R).val

Tactic:
roots_prod_X_sub_C (primitiveRoots n R)

Premises used: primitiveRoots, Polynomial.roots_prod_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
⊢ roots (∏ μ ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X])) =
    (primitiveRoots n R).val

Tactic:
exact roots_prod_X_sub_C (primitiveRoots n R)

Premises used: primitiveRoots, Polynomial.roots_prod_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
rw :
  HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ : Finset R },
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
⊢ HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])

Tactic:
rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]

Premises used: IsPrimitiveRoot.nthRoots_one_nodup, Polynomial.nthRootsFinset, Multiset.toFinset_eq
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic

Tactic:
have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic
symm :
  Multiset.prod
      (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X]))
        (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots) =
    HPow.hPow (α := R[X]) X n - 1
⊢ HPow.hPow (α := R[X]) X n - 1 =
    Multiset.prod
      (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X]))
        (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots)

Tactic:
symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic
apply :
  (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots.card =
    (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).natDegree
⊢ Multiset.prod
      (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X]))
        (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots) =
    HPow.hPow (α := R[X]) X n - 1

Tactic:
apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic

Premises used: Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic
rw : Multiset.card.{u_1} (α := R) (nthRoots n 1) = n
⊢ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots.card =
    (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).natDegree

Tactic:
rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]

Premises used: Polynomial.natDegree_X_pow_sub_C, Polynomial.nthRoots
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic
⊢ Multiset.card.{u_1} (α := R) (nthRoots n 1) = n

Tactic:
IsPrimitiveRoot.card_nthRoots_one h

Premises used: IsPrimitiveRoot.card_nthRoots_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic
⊢ Multiset.card.{u_1} (α := R) (nthRoots n 1) = n

Tactic:
exact IsPrimitiveRoot.card_nthRoots_one h

Premises used: IsPrimitiveRoot.card_nthRoots_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
rw :
  HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ Multiset.toFinset (nthRoots n 1), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
rw₁ rw₂ rw₃ :
  HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ { val := nthRoots n 1, nodup := ⋯ : Finset R },
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
rw₄ :
  HPow.hPow (α := R[X]) X n - 1 =
    Multiset.prod
      (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])) (nthRoots n 1))
rw₅ :
  HPow.hPow (α := R[X]) X n - 1 =
    Multiset.prod
      (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X]))
        (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots)
rw₆ :
  ∀ (hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic),
    HPow.hPow (α := R[X]) X n - 1 =
      Multiset.prod
        (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X]))
          (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots)
rw₇ :
  ∀ (hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic),
    Multiset.prod
        (Multiset.map (fun (ζ : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X]))
          (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots) =
      HPow.hPow (α := R[X]) X n - 1
rw₈ :
  ∀ (hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic),
    (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots.card =
      (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).natDegree
rw₉ :
  ∀ (hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic),
    Multiset.card.{u_1} (α := R) (nthRoots n 1) = n
⊢ HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])

Tactic:
classical
  rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]
  simp only [Finset.prod_mk]
  rw [nthRoots]
  have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
  symm
  apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
  rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
  exact IsPrimitiveRoot.card_nthRoots_one h

Premises used: Polynomial.natDegree_X_pow_sub_C, Finset.prod_mk, Polynomial.nthRoots, Polynomial.nthRootsFinset, IsPrimitiveRoot.card_nthRoots_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : Field K
n : ℕ
h : ∀ i ∈ primitiveRoots n K, (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) i : K[X])).Splits
⊢ Splits (cyclotomic' n K)

Tactic:
apply Splits.prod

Premises used: Polynomial.Splits.prod
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : Field K
n : ℕ
z : K
h : z ∈ primitiveRoots n K → (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])).Splits
⊢ z ∈ primitiveRoots n K → (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])).Splits

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : Field K
n : ℕ
z : K
h : z ∈ primitiveRoots n K
⊢ (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])).Splits

Tactic:
simp only [Splits.X_sub_C]

Premises used: Polynomial.Splits.X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_1
inst : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
rw :
  (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).roots.card =
    (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).natDegree
rw₁ : Multiset.card.{u_1} (α := K) (nthRoots n 1) = (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).natDegree
rw₂ : n = (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).natDegree
rw₃ rw₄ : n = n
⊢ (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).Splits

Tactic:
rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]

Premises used: Polynomial.natDegree_X_pow_sub_C, Polynomial.splits_iff_card_roots, Polynomial.nthRoots, IsPrimitiveRoot.card_nthRoots_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ Set.PairwiseDisjoint.{u_2, 0} (α := Finset K) (↑n.divisors : Set ℕ) fun (k : ℕ) ↦ primitiveRoots k K

Tactic:
have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K :=
    fun x _ y _ hne => IsPrimitiveRoot.disjoint hne
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hd : Set.PairwiseDisjoint.{u_2, 0} (α := Finset K) (↑n.divisors : Set ℕ) fun (k : ℕ) ↦ primitiveRoots k K
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = HPow.hPow (α := K[X]) X n - 1

Tactic:
simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
    IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots]

Premises used: IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots, Finset.prod_biUnion, Polynomial.X_pow_sub_one_eq_prod, Polynomial.cyclotomic'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
have have₁ have₂ :
  ∀ (hd : Set.PairwiseDisjoint.{u_2, 0} (α := Finset K) (↑n.divisors : Set ℕ) fun (k : ℕ) ↦ primitiveRoots k K),
    ∏ i ∈ n.divisors, cyclotomic' i K = HPow.hPow (α := K[X]) X n - 1
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = HPow.hPow (α := K[X]) X n - 1

Tactic:
classical
  have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K :=
    fun x _ y _ hne => IsPrimitiveRoot.disjoint hne
  simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
    IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots]

Premises used: IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots, Polynomial.X_pow_sub_one_eq_prod, Polynomial.cyclotomic'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
rw :
  cyclotomic' n K =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic' i K
⊢ cyclotomic' n K = (HPow.hPow (α := K[X]) X n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
rw [← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← 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:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hs : ∀ i ∈ n.properDivisors, Monic (cyclotomic' i K)
⊢ Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)

Tactic:
apply monic_prod_of_monic

Premises used: Polynomial.monic_prod_of_monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
hs : i ∈ n.properDivisors → Monic (cyclotomic' i K)
⊢ i ∈ n.properDivisors → Monic (cyclotomic' i K)

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
h_1 : i ∈ n.properDivisors
⊢ Monic (cyclotomic' i K)

Tactic:
cyclotomic'.monic i K

Premises used: Polynomial.cyclotomic'.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
h_1 : i ∈ n.properDivisors
⊢ Monic (cyclotomic' i K)

Tactic:
exact cyclotomic'.monic i K

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

Tactic:
have prod_monic : (∏ i ∈ Nat.properDivisors n, cyclotomic' i K).Monic := by
    apply monic_prod_of_monic
    intro i _
    exact cyclotomic'.monic i K
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
rw :
  0 + HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
      HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) ∧
    degree.{u_2} (R := K) 0 < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
⊢ cyclotomic' n K =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic' i K

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

Premises used: Polynomial.div_modByMonic_unique, And.left, Polynomial.cyclotomic', OfNat.ofNat