awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
s : S
⊢ s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
have pos : ∀ (hs : s = 0),
  s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
Tactic: by_cases hs : s = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
s : S
pos :
  ∀ (hs : s = 0),
    s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
      Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
⊢ s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
have neg : ∀ (hs : ¬s = 0),
  s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
Tactic: by_cases hs : s = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
⊢ (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal
have rw : (↑(p * q).coeffs : Set R) ⊆ (↑(p.contentIdeal * q.contentIdeal) : Set R)
Tactic: rw [contentIdeal_def, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
⊢ (↑(p * q).coeffs : Set R) ⊆ (↑(p.contentIdeal * q.contentIdeal) : Set R)
have simp : ∀ (x : R), (∃ n ∈ (p * q).support, x = (p * q).coeff n) → x ∈ (↑(p.contentIdeal * q.contentIdeal) : Set R)
Tactic: simp only [Set.subset_def, Finset.mem_coe, mem_coeffs_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
hpq : p ∣ q
⊢ q.contentIdeal ≤ p.contentIdeal
have obtain : ∀ (p' : R[X]), (p * p').contentIdeal ≤ p.contentIdeal
Tactic: obtain ⟨p', rfl⟩ := hpq
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
have this : p.coeff n ∈ p.contentIdeal
Tactic: have := p.coeff_mem_contentIdeal n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : p.coeff n ∈ p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
have this₁ : ∃ (s : R), p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal
Tactic: rw [Submodule.IsPrincipal.mem_iff_eq_smul_generator] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : ∃ (s : R), p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
have obtain : ∀ (w : R) (ha : p.coeff n = w • Submodule.IsPrincipal.generator p.contentIdeal),
  Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
Tactic: obtain ⟨_, ha⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ (C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p
have rw : ∀ (i : ℕ), Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff i
Tactic: rw [C_dvd_iff_dvd_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ p.contentIdeal ≤ span {r} ↔ (C : (a : R) → R[X]) r ∣ p
have mp : p.contentIdeal ≤ span {r} → (C : (a : R) → R[X]) r ∣ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
mp : p.contentIdeal ≤ span {r} → (C : (a : R) → R[X]) r ∣ p
⊢ p.contentIdeal ≤ span {r} ↔ (C : (a : R) → R[X]) r ∣ p
have mpr : (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ span {r}
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ p.contentIdeal ≤ span {r} → (C : (a : R) → R[X]) r ∣ p
have mp : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r}) → (C : (a : R) → R[X]) r ∣ p
Tactic: rw [← p.contentIdeal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
h : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r})
⊢ Dvd.dvd (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    ((C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) : R[X])
have apply : r ∣ Submodule.IsPrincipal.generator p.contentIdeal
Tactic: apply _root_.map_dvd C
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
h : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r})
⊢ (C : (a : R) → R[X]) r ∣ p
have C : Dvd.dvd (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
  ((C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) : R[X])
Tactic: calc
    C r ∣ C h_prin.generator := by
      apply _root_.map_dvd C
      rwa [← span_singleton_le_span_singleton]
     _ ∣ p := h_prin.contentIdeal_generator_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ span {r}
have mpr : (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ contentIdeal ((C : (a : R) → R[X]) r)
Tactic: rw [← contentIdeal_C r]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal p.contentIdeal
have rw : Submodule.IsPrincipal.{u_3, u_3} (R := R) (M := R) ⊤
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ p.IsPrimitive
have h_prin : Submodule.IsPrincipal p.contentIdeal
Tactic: have h_prin : p.contentIdeal.IsPrincipal := by
    rw [h]
    exact top_isPrincipal
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive ↔ p.contentIdeal = ⊤
have refine : p.IsPrimitive → p.contentIdeal = ⊤
Tactic: refine ⟨?_, fun h ↦ isPrimitive_of_contentIdeal_eq_top h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive → p.contentIdeal = ⊤
have contrapose! : p.contentIdeal ≠ ⊤ → ¬p.IsPrimitive
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal ≠ ⊤ → ¬p.IsPrimitive
have simp : p.contentIdeal ≠ ⊤ → ∃ (x : R) (_ : (C : (a : R) → R[X]) x ∣ p), ¬IsUnit x
Tactic: simp only [IsPrimitive, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
h : p.contentIdeal ≠ ⊤
⊢ ∃ (x : R) (_ : (C : (a : R) → R[X]) x ∣ p), ¬IsUnit x
have h : ¬IsUnit (Submodule.IsPrincipal.generator p.contentIdeal)
Tactic: use h_prin.generator, h_prin.contentIdeal_generator_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ p.contentIdeal = ⊤
have apply : ⊤ ≤ p.contentIdeal
Tactic: apply le_antisymm le_top
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
⊢ p.contentIdeal * q.contentIdeal ≤ (p * q).contentIdeal.radical
have rw : ∀ (b : Ideal R),
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | (p * q).contentIdeal ≤ J ∧ J.IsPrime} b →
    p.contentIdeal * q.contentIdeal ≤ b
Tactic: rw [radical_eq_sInf, le_sInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) {J : Ideal R | (p * q).contentIdeal ≤ J ∧ J.IsPrime} P →
    p.contentIdeal * q.contentIdeal ≤ P
have this : ∀ (hpq : (p * q).contentIdeal ≤ P) (hPprime : P.IsPrime), p.contentIdeal * q.contentIdeal ≤ P
Tactic: ⟨hpq, hPprime⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
⊢ p.contentIdeal * q.contentIdeal ≤ P
have rw : p.contentIdeal ≤ P ∨ q.contentIdeal ≤ P
Tactic: rw [hPprime.mul_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
⊢ p.contentIdeal ≤ P ∨ q.contentIdeal ≤ P
have rw : ∀ (hpq : (p * q).contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P)) (hPprime : P.IsPrime),
  p.contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) ∨
    q.contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P)
Tactic: rw [← Ideal.mk_ker (I := P)] at hpq ⊢
Cleared hypotheses: hpq, hPprime
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ (p * q).contentIdeal = ⊤
have rw : (p * q).contentIdeal.radical = ⊤
Tactic: rw [← Ideal.radical_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ (p * q).contentIdeal.radical = ⊤
have apply : ⊤ ≤ (p * q).contentIdeal.radical
Tactic: apply le_antisymm le_top
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ ⊤ ≤ (p * q).contentIdeal.radical
have by : ⊤ = p.contentIdeal * q.contentIdeal
Tactic: calc
    ⊤ = p.contentIdeal * q.contentIdeal := by simp [hp, hq]
    _ ≤ ((p * q).contentIdeal).radical := mul_contentIdeal_le_radical_contentIdeal_mul
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ p.contentIdeal ≤ span {p.content}
have rw : (↑p.coeffs : Set R) ⊆ (↑(span {p.content}) : Set R)
Tactic: rw [contentIdeal_def, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : R
h1 : a ∈ (↑p.coeffs : Set R)
⊢ a ∈ (↑(span {p.content}) : Set R)
have h1₁ : ∃ n ∈ p.support, a = p.coeff n
Tactic: rw [Finset.mem_coe, mem_coeffs_iff] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
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
⊢ a ∈ (↑(span {p.content}) : Set R)
have obtain : ∀ n ∈ p.support, ∀ (h2 : a = p.coeff n), a ∈ (↑(span {p.content}) : Set R)
Tactic: obtain ⟨n, _, h2⟩ := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
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
⊢ a ∈ (↑(span {p.content}) : Set R)
have rw : p.content ∣ p.coeff n
Tactic: rw [SetLike.mem_coe, h2, mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal = span {p.content}
have apply : span {p.content} ≤ p.contentIdeal
Tactic: apply le_antisymm contentIdeal_le_span_content
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ span {p.content} ≤ p.contentIdeal
have rw : ∀ b ∈ p.support, Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff b
Tactic: rw [← p.contentIdeal.span_singleton_generator, span_singleton_le_span_singleton, content,
    Finset.dvd_gcd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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}
have simp : IsPrimitiveRoot.{u_2} (M := R) (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1
Tactic: simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : CharP R p
hp : p ≠ 2
⊢ ∏ μ ∈ primitiveRoots 2 R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]) =
    HAdd.hAdd (α := R[X]) X 1
have prim_root_two : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ natDegree (R := R) (∏ μ ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X])) =
    n.totient
have rw : ∑ i ∈ primitiveRoots n R, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).natDegree = n.totient
Tactic: rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ natDegree (R := R) (∏ μ ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X])) =
    n.totient
have rw₁ : ∀ i ∈ primitiveRoots n R, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X]) ≠ 0
Tactic: rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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 - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
have rw : HPow.hPow (α := R[X]) X n - 1 =
  ∏ ζ ∈ { val := nthRoots n 1, nodup := sorry : Finset R },
    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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
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 - 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)
have hmonic : (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ 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)
have 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
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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.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
have 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
Tactic: apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ (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
have rw : Multiset.card.{u_1} (α := R) (nthRoots n 1) = n
Tactic: rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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 - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
have 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])
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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])
⊢ HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
have rw₁ : HPow.hPow (α := R[X]) X n - 1 =
  ∏ ζ ∈ { val := nthRoots n 1, nodup := sorry : Finset R },
    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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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])
⊢ HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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))
⊢ HPow.hPow (α := R[X]) X n - 1 =
    ∏ ζ ∈ nthRootsFinset n 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) ζ : R[X])
have 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)
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