awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this_2 : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
this : LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
⊢ P * P ∣ cyclotomic n K
have this₁ : Dvd.dvd (α := K[X]) (prod {P, P}) (prod (normalizedFactors (cyclotomic n K)))
Tactic: have := prod_dvd_prod_of_le this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this_2 : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
this_3 : LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
this : Dvd.dvd (α := K[X]) (prod {P, P}) (prod (normalizedFactors (cyclotomic n K)))
⊢ P * P ∣ cyclotomic n K
have this₁ : P * P ∣ prod (normalizedFactors (cyclotomic n K))
Tactic: simp only [insert_eq_cons, prod_cons, prod_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1
have inl : ∀ (hi : i ∈ Nat.divisors 0), HPow.hPow (β := ℕ) ζ 0 = 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n, hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
inl : ∀ (hi : i ∈ Nat.divisors 0), HPow.hPow (β := ℕ) ζ 0 = 1
⊢ ζ ^ n = 1
have inr : ∀ (hn : n > 0), ζ ^ n = 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
⊢ ζ ^ n = 1
have this : eval ζ (HPow.hPow (α := R[X]) X n - 1) = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
Tactic: have := congr_arg (eval ζ) (prod_cyclotomic_eq_X_pow_sub_one hn R).symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : eval ζ (HPow.hPow (α := R[X]) X n - 1) = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ ζ ^ n = 1
have this₁ : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
Tactic: rw [eval_sub, eval_X_pow, eval_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ 1 = 1 + eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
have h₁ : eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0
Tactic: convert! (add_zero (M := R) _).symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0
have apply : Dvd.dvd (α := R[X]) (cyclotomic i R) (∏ i ∈ n.divisors, cyclotomic i R)
Tactic: apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
ζ : R
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
have rw : Membership.mem (γ := Multiset R) (nthRoots n 1) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
Tactic: rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
      prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
ζ : R
rw : Membership.mem (γ := Multiset R) (nthRoots n 1) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
have rw₁ : ζ ∈ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
Tactic: rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
      prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
ζ : R
rw : Membership.mem (γ := Multiset R) (nthRoots n 1) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₁ : ζ ∈ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
have rw₂ : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
Tactic: rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
      prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
ζ : R
rw : Membership.mem (γ := Multiset R) (nthRoots n 1) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₁ : ζ ∈ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₂ : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
have rw₃ : (HPow.hPow (α := R[X]) X n - 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
Tactic: rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
      prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
ζ : R
rw : Membership.mem (γ := Multiset R) (nthRoots n 1) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₁ : ζ ∈ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₂ : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₃ : (HPow.hPow (α := R[X]) X n - 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
have rw₄ : IsRoot (∏ i ∈ n.divisors, cyclotomic i R) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
Tactic: rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
      prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
h : 0 < n
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
ζ : R
rw : Membership.mem (γ := Multiset R) (nthRoots n 1) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₁ : ζ ∈ (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).roots ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₂ : (HPow.hPow (α := R[X]) X n - (C : (a : R) → R[X]) 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₃ : (HPow.hPow (α := R[X]) X n - 1).IsRoot ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
rw₄ : IsRoot (∏ i ∈ n.divisors, cyclotomic i R) ζ ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
have rw₅ : (∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ) ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
Tactic: rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
      prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ IsRoot (cyclotomic n R) μ
have rw : μ ∈ primitiveRoots n R
Tactic: rw [← mem_roots (cyclotomic_ne_zero n R), cyclotomic_eq_prod_X_sub_primitiveRoots h,
    roots_prod_X_sub_C, ← Finset.mem_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R
have rwa : ∀ (h : μ ∈ primitiveRoots n R), μ ∈ primitiveRoots n R
Tactic: rwa [← mem_primitiveRoots hpos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n
have hnpos : 0 < n
Tactic: have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n
have refine : ∀ (hμ : IsRoot (cyclotomic n K) μ), IsPrimitiveRoot μ n
Tactic: refine ⟨fun hμ => ?_, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ μ ^ n = 1
have rw : ∃ i ∈ n.divisors, IsRoot (cyclotomic i K) μ
Tactic: rw [isRoot_of_unity_iff hnpos _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
⊢ IsPrimitiveRoot μ n
have hμn : μ ^ n = 1
Tactic: have hμn : μ ^ n = 1 := by
    rw [isRoot_of_unity_iff hnpos _]
    exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
⊢ IsPrimitiveRoot μ n
have by_contra : ∀ (hnμ : ¬IsPrimitiveRoot μ n), False
Tactic: by_contra hnμ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ False
have ho : 0 < orderOf μ
Tactic: have ho : 0 < orderOf μ := (isOfFinOrder_iff_pow_eq_one.2 <| ⟨n, hnpos, hμn⟩).orderOf_pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
⊢ False
have this : μ ^ orderOf μ = 1
Tactic: have := pow_orderOf_eq_one μ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : μ ^ orderOf μ = 1
⊢ False
have this₁ : ∃ i ∈ (orderOf μ).divisors, IsRoot (cyclotomic i K) μ
Tactic: rw [isRoot_of_unity_iff ho] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : ∃ i ∈ (orderOf μ).divisors, IsRoot (cyclotomic i K) μ
⊢ False
have obtain : ∀ (i : ℕ) (hio : i ∈ (orderOf μ).divisors) (hiμ : IsRoot (cyclotomic i K) μ), False
Tactic: obtain ⟨i, hio, hiμ⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∈ (orderOf μ).divisors
hiμ : IsRoot (cyclotomic i K) μ
⊢ False
have hio₁ : i ∣ orderOf μ
Tactic: replace hio := Nat.dvd_of_mem_divisors hio
Cleared hypotheses: hio
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
have rw : ∀ (hnμ : orderOf μ ≠ n) (ho : 0 < orderOf μ) (i : ℕ) (hiμ : IsRoot (cyclotomic i K) μ) (hio : i ∣ orderOf μ), False
Tactic: rw [IsPrimitiveRoot.not_iff] at hnμ
Cleared hypotheses: hnμ, ho, i, hiμ, hio
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : μ ^ n = 1
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
have rw : ∀ (hμn : orderOf μ ∣ n) (hnμ : orderOf μ ≠ n) (ho : 0 < orderOf μ) (i : ℕ) (hiμ : IsRoot (cyclotomic i K) μ)
  (hio : i ∣ orderOf μ), False
Tactic: rw [← orderOf_dvd_iff_pow_eq_one] at hμn
Cleared hypotheses: hμn, hnμ, ho, i, hiμ, hio
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
⊢ False
have key : i < n
Tactic: have key : i < n := (Nat.le_of_dvd ho hio).trans_lt ((Nat.le_of_dvd hnpos hμn).lt_of_ne hnμ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
key : i < n
⊢ False
have key' : i ∣ n
Tactic: have key' : i ∣ n := hio.trans hμn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : IsRoot (cyclotomic n K) μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : IsRoot (cyclotomic i K) μ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
have rw : ∀ (hμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic n K) (hμn : orderOf μ ∣ n)
  (hnμ : orderOf μ ≠ n) (ho : 0 < orderOf μ) (i : ℕ)
  (hiμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic i K) (hio : i ∣ orderOf μ)
  (key : i < n) (key' : i ∣ n), False
Tactic: rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ
Cleared hypotheses: hμ, hμn, hnμ, ho, i, hiμ, hio, key, key'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
have hni : {i, n} ⊆ n.divisors
Tactic: have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
⊢ False
have obtain : ∀ (k : K[X]) (hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k), False
Tactic: obtain ⟨k, hk⟩ := hiμ
Cleared hypotheses: hiμ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (goal)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμ : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k
⊢ False
have obtain : ∀ (j : K[X]) (hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j), False
Tactic: obtain ⟨j, hj⟩ := hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k
j : K[X]
hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j
⊢ False
have this : ∏ i ∈ n.divisors, cyclotomic i K = HPow.hPow (α := K[X]) X n - 1
Tactic: have := prod_cyclotomic_eq_X_pow_sub_one hnpos K
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k
j : K[X]
hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j
this : ∏ i ∈ n.divisors, cyclotomic i K = HPow.hPow (α := K[X]) X n - 1
⊢ False
have this₁ : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) *
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j)) =
  HPow.hPow (α := K[X]) X n - 1
Tactic: rw [← Finset.prod_sdiff hni, Finset.prod_pair key.ne, hk, hj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k
j : K[X]
hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j
this :
  (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j)) =
    HPow.hPow (α := K[X]) X n - 1
⊢ False
have hn : Squarefree (HPow.hPow (α := K[X]) X n - 1)
Tactic: have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k
j : K[X]
hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j
this :
  (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j)) =
    HPow.hPow (α := K[X]) X n - 1
hn : Squarefree (HPow.hPow (α := K[X]) X n - 1)
⊢ False
have hn₁ : ∀ (x : K[X]),
  x * x ∣
      (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k *
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j)) →
    IsUnit x
Tactic: rw [← this, Squarefree] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k
j : K[X]
hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j
this :
  (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j)) =
    HPow.hPow (α := K[X]) X n - 1
hn :
  ∀ (x : K[X]),
    x * x ∣
        (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) *
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k *
            (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j)) →
      IsUnit x
⊢ False
have hn₁ : IsUnit (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))
Tactic: specialize hn (X - C μ) ⟨(∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * k * j, by ring⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
have hf : Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)
Tactic: have hf : Function.Injective _ := IsFractionRing.injective R (FractionRing R)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
hf : Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)
⊢ IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n
have this : NeZero.{u_1} (R := FractionRing R) (↑n : FractionRing R)
Tactic: haveI : NeZero (n : FractionRing R) := NeZero.nat_of_injective hf