awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inl :
  Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic 0 R) : RatFunc R)
    (∏ i ∈ Nat.divisorsAntidiagonal 0,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
have inr : ∀ (hpos : n > 0),
  Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n_1 > 0
n : ℕ
hn : 0 < n
⊢ Eq (α := RatFunc R)
    (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
    ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
have rw : Eq.{u_1 + 1} (α := RatFunc R)
  (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R))
  ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (∏ i ∈ n.divisors, cyclotomic i R))
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n_1 > 0
n : ℕ
hn : 0 < n
rw :
  Eq.{u_1 + 1} (α := RatFunc R)
    (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R))
    ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (∏ i ∈ n.divisors, cyclotomic i R))
⊢ Eq (α := RatFunc R)
    (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
    ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
have rw₁ : Eq.{u_1 + 1} (α := RatFunc R)
  (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R))
  (∏ x ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic x R))
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
have h : ∀ (n : ℕ),
  0 < n →
    Eq (α := RatFunc R)
      (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
      ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
Tactic: have h : ∀ n : ℕ, 0 < n → (∏ i ∈ Nat.divisors n, algebraMap _ (RatFunc R) (cyclotomic i R)) =
      algebraMap _ _ (X ^ n - 1 : R[X]) := by
    intro n hn
    rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
have rw : ∀ (n : ℕ) (hn : 0 < n),
  Ne (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (0 : RatFunc R)
Tactic: rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
rw :
  ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
      (0 : RatFunc R)
⊢ Eq (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
    (∏ i ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := RatFunc R) (β := ℤ)
          ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X i.2 - 1) : RatFunc R)
          ((μ : (a : ℕ) → ℤ) i.1 : ℤ) :
      RatFunc R)
have rw₁ : ∀ (n : ℕ) (hn : 0 < n),
  Ne (α := RatFunc R)
    ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R) (0 : RatFunc R)
Tactic: rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
⊢ ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R) ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic n R) : RatFunc R)
      (0 : RatFunc R)
have simp_rw : ∀ (n : ℕ) (hn : 0 < n), ¬Eq (α := R[X]) (cyclotomic n R) 0
Tactic: simp_rw [Ne, IsFractionRing.to_map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
⊢ ∀ (n : ℕ) (hn : 0 < n),
    Ne (α := RatFunc R)
      ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
      (0 : RatFunc R)
have simp_rw : ∀ (n : ℕ) (hn : 0 < n), ¬HPow.hPow (α := R[X]) X n - 1 = 0
Tactic: simp_rw [Ne, IsFractionRing.to_map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hpos : n_1 > 0
h :
  ∀ (n : ℕ),
    0 < n →
      Eq (α := RatFunc R)
        (∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (cyclotomic i R) : RatFunc R)
        ((algebraMap R[X] (RatFunc R) : (a : R[X]) → RatFunc R) (HPow.hPow (α := R[X]) X n - 1) : RatFunc R)
n : ℕ
hn : 0 < n
⊢ ¬HPow.hPow (α := R[X]) X n - 1 = 0
have hp : (HPow.hPow (α := R[X]) X n - 1).Monic
Tactic: apply Monic.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
⊢ cyclotomic n R = (HPow.hPow (α := R[X]) X n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
⊢ cyclotomic n R = (HPow.hPow (α := R[X]) X n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
have rw : cyclotomic n R =
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ
    ∏ i ∈ n.properDivisors, cyclotomic i R
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos, ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
⊢ Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
have hs : ∀ i ∈ n.properDivisors, Monic (cyclotomic i R)
Tactic: apply monic_prod_of_monic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
h : Nontrivial R
⊢ cyclotomic n R =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic i R
have prod_monic : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ cyclotomic n R =
    HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ
      ∏ i ∈ n.properDivisors, cyclotomic i R
have 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)
Tactic: rw [(div_modByMonic_unique (cyclotomic n R) 0 prod_monic _).1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: simp only [degree_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ 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)
have right : ⊥ < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ ⊥ < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
have right : degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R) ≠ ⊥
Tactic: rw [bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n m : ℕ
hpos : 0 < n
hm : m ∣ n
hdiff : m ≠ n
⊢ HPow.hPow (α := R[X]) X m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R
have hm₁ : 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⟩
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R
have rw : HPow.hPow (α := R[X]) X m - 1 ∣ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (HPow.hPow (α := R[X]) X m - 1)
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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ (∏ 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
have 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
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ Eq (α := K[X]) (cyclotomic n K) (cyclotomic' n K)
have 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)
Tactic: induction n using Nat.strong_induction_on generalizing ζ with | _ k hk
Cleared hypotheses: ζ, n, hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
have h : ∀ (hzero : k = 0), Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
Tactic: obtain hzero | hpos := k.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
have h₁ : ∀ (hpos : k > 0), Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
Tactic: obtain hzero | hpos := k.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)
have obtain : ∀ (d : ℕ) (hd : k = i * d), Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)
Tactic: obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hi).1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
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
⊢ Eq (α := K[X]) (cyclotomic i K) (cyclotomic' i K)
have hd₁ : k = d * i
Tactic: rw [mul_comm] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
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
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
have h : ∀ 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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)
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
have h₁ : (HPow.hPow (α := K[X]) X k - 1) /ₘ ∏ i ∈ k.properDivisors, cyclotomic i 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ Eq (α := K[X]) (cyclotomic k K) (cyclotomic' k K)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
⊢ P = cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
have refine_1 : ∀ (hcycl : P = cyclotomic n R), P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
Tactic: refine ⟨fun hcycl => ?_, fun hP => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ P = cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have refine_2 : ∀ (hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1), P = cyclotomic n R
Tactic: refine ⟨fun hcycl => ?_, fun hP => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have refine_1 : HMul.hMul (α := R[X]) (cyclotomic n R) (∏ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have refine_1₁ : HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) = ∏ i ∈ n.divisors, cyclotomic i R
Tactic: rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← Nat.cons_self_properDivisors hpos.ne',
      Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
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
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have refine_1₂ : HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) =
  ∏ i ∈ cons n n.properDivisors sorry, cyclotomic i R
Tactic: rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← Nat.cons_self_properDivisors hpos.ne',
      Finset.prod_cons]