awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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)
⊢ 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₆ : ∀ (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)
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))
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)
⊢ 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₇ : ∀ (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
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))
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
⊢ 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₈ : ∀ (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
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))
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
⊢ 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₉ : ∀ (hmonic : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).Monic), Multiset.card.{u_1} (α := R) (nthRoots n 1) = n
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:
K : Type u_1
inst : Field K
n : ℕ
⊢ Splits (cyclotomic' n K)
have h : ∀ i ∈ primitiveRoots n K, (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) i : K[X])).Splits
Tactic: apply Splits.prod
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).Splits
have 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
Tactic: rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).Splits
have rw₁ : Multiset.card.{u_1} (α := K) (nthRoots n 1) = (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).natDegree
Tactic: rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).Splits
have rw₂ : n = (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).natDegree
Tactic: rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 1).Splits
have rw₃ : n = n
Tactic: rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = HPow.hPow (α := K[X]) X n - 1
have hd : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∏ i ∈ n.divisors, cyclotomic' i K = HPow.hPow (α := K[X]) X n - 1
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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (HPow.hPow (α := K[X]) X n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
have rw : cyclotomic' n K =
  HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ
    ∏ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
have hs : ∀ i ∈ n.properDivisors, Monic (cyclotomic' i K)
Tactic: apply monic_prod_of_monic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic' i K
have prod_monic : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ cyclotomic' n K =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic' i K
have 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)
Tactic: rw [(div_modByMonic_unique (cyclotomic' n K) 0 prod_monic _).1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ 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)
have simp : HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K) ∧
  ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
Tactic: simp only [degree_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
have rw : HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K) =
  HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
      HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K) ∧
    ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
have refine : ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
Tactic: refine ⟨by rw [mul_comm], ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
have rw : degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K) ≠ ⊥
Tactic: rw [bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∃ (P : ℤ[X]),
    Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' n K) ∧ P.degree = degree (cyclotomic' n K) ∧ P.Monic
have refine : Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' n K)
Tactic: refine lifts_and_degree_eq_and_monic ?_ (cyclotomic'.monic n K)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' n K)
have h₁ : ∀ (k : ℕ)
  (ihk :
    ∀ m < k,
      ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
        Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K))
  {ζ : K} (h : IsPrimitiveRoot ζ k),
  Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
Tactic: induction n using Nat.strong_induction_on generalizing ζ with | _ k ihk
Cleared hypotheses: ζ, n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have h₁ : ∀
  (ihk :
    ∀ m < 0,
      ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
        Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K))
  (h : IsPrimitiveRoot ζ 0),
  Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' 0 K)
Tactic: rcases k.eq_zero_or_pos with (rfl | hpos)
Cleared hypotheses: k, ihk, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
h₁ :
  ∀
    (ihk :
      ∀ m < 0,
        ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
          Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K))
    (h : IsPrimitiveRoot ζ 0),
    Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' 0 K)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have h₂ : ∀ (hpos : k > 0), Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
Tactic: rcases k.eq_zero_or_pos with (rfl | hpos)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
ihk :
  ∀ m < 0,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
h : IsPrimitiveRoot ζ 0
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' 0 K)
have h₁ : Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) 1 : K[X]) (cyclotomic' 0 K : K[X])
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
⊢ B.Monic
have hs : ∀ i ∈ k.properDivisors, Monic (cyclotomic' i K)
Tactic: apply monic_prod_of_monic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
have Bmo : B.Monic
Tactic: have Bmo : B.Monic := by
    apply monic_prod_of_monic
    intro i _
    exact cyclotomic'.monic i K
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B
have refine : ∀ c ∈ k.properDivisors, Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' c K)
Tactic: refine Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)
have xsmall : x < k
Tactic: have xsmall := (Nat.mem_properDivisors.1 hx).2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)
have obtain : ∀ (d : ℕ) (hd : k = x * d),
  Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)
Tactic: obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1