awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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 : P * P ∣ prod (normalizedFactors (cyclotomic n K))
⊢ P * P ∣ cyclotomic n K

Tactic:
exact this.trans h.dvd

Premises used: Associated.dvd, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
inr : ∀ (hn : n > 0), ζ ^ n = 1
⊢ ζ ^ n = 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
ζ : R
i : ℕ
h : IsRoot (cyclotomic i R) ζ
hi : i ∈ Nat.divisors 0
⊢ HPow.hPow (β := ℕ) ζ 0 = 1

Tactic:
pow_zero _

Premises used: pow_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
ζ : R
i : ℕ
h : IsRoot (cyclotomic i R) ζ
hi : i ∈ Nat.divisors 0
⊢ HPow.hPow (β := ℕ) ζ 0 = 1

Tactic:
exact pow_zero _

Premises used: pow_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : IsRoot (cyclotomic i R) ζ
hn : n > 0
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
rw [eval_sub, eval_X_pow, eval_one] at this

Premises used: Polynomial.eval_X_pow, Polynomial.eval_one, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ ζ ^ n = 1 + eval ζ (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
eq_add_of_sub_eq' this

Premises used: eq_add_of_sub_eq'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 = HAdd.hAdd (α := R) 1 0

Tactic:
(add_zero (M := R) _).symm

Premises used: add_zero, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
h₁ : eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0
⊢ 1 = 1 + eval ζ (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
convert! (add_zero (M := R) _).symm

Premises used: add_zero, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
apply : Dvd.dvd (α := R[X]) (cyclotomic i R) (∏ i ∈ n.divisors, cyclotomic i R)
⊢ eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0

Tactic:
apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h

Premises used: Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ Dvd.dvd (α := R[X]) (cyclotomic i R) (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
Finset.dvd_prod_of_mem _ hi

Premises used: Finset.dvd_prod_of_mem
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ Dvd.dvd (α := R[X]) (cyclotomic i R) (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
exact Finset.dvd_prod_of_mem _ hi

Premises used: Finset.dvd_prod_of_mem
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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) ζ
rw₅ rw₆ : (∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ) ↔ ∃ i ∈ n.divisors, IsRoot (cyclotomic i R) ζ
⊢ ζ ^ 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]

Premises used: Polynomial.C_1, Polynomial.prod_cyclotomic_eq_X_pow_sub_one, Polynomial.nthRoots, Polynomial.mem_roots, Polynomial.isRoot_prod, Polynomial.mem_nthRoots, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
rw : μ ∈ primitiveRoots n R
⊢ IsRoot (cyclotomic 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]

Premises used: Polynomial.cyclotomic_ne_zero, Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots, Polynomial.mem_roots, Finset.mem_def, Polynomial.roots_prod_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : μ ∈ primitiveRoots n R), μ ∈ primitiveRoots n R
⊢ μ ∈ primitiveRoots n R

Tactic:
rwa [← mem_primitiveRoots hpos] at h

Premises used: mem_primitiveRoots
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
⊢ 0 < n

Tactic:
have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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

Tactic:
⟨fun hμ => ?_, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩

Premises used: Iff.intro, IsPrimitiveRoot.isRoot_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
K : Type u_2
inst : Field K
μ : K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
hnpos : 0 < n
refine : ∀ (hμ : IsRoot (cyclotomic n K) μ), IsPrimitiveRoot μ n
⊢ IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n

Tactic:
refine ⟨fun hμ => ?_, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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) μ
rw : ∃ i ∈ n.divisors, IsRoot (cyclotomic i K) μ
⊢ μ ^ n = 1

Tactic:
rw [isRoot_of_unity_iff hnpos _]

Premises used: isRoot_of_unity_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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) μ
⊢ ∃ i ∈ n.divisors, IsRoot (cyclotomic i K) μ

Tactic:
⟨n, n.mem_divisors_self hnpos.ne', hμ⟩

Premises used: LT.lt.ne', And.intro, Exists.intro, Nat.mem_divisors_self
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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) μ
⊢ ∃ i ∈ n.divisors, IsRoot (cyclotomic i K) μ

Tactic:
exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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

Tactic:
have hμn : μ ^ n = 1 := by
    rw [isRoot_of_unity_iff hnpos _]
    exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
by_contra : ∀ (hnμ : ¬IsPrimitiveRoot μ n), False
⊢ IsPrimitiveRoot μ n

Tactic:
by_contra hnμ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ 0 < orderOf μ

Tactic:
have ho : 0 < orderOf μ := (isOfFinOrder_iff_pow_eq_one.2 <| ⟨n, hnpos, hμn⟩).orderOf_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 μ
⊢ μ ^ orderOf μ = 1

Tactic:
have := pow_orderOf_eq_one μ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ ∃ i ∈ (orderOf μ).divisors, IsRoot (cyclotomic i K) μ

Tactic:
rw [isRoot_of_unity_iff ho] at this

Premises used: isRoot_of_unity_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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) μ
obtain : ∀ (i : ℕ) (hio : i ∈ (orderOf μ).divisors) (hiμ : IsRoot (cyclotomic i K) μ), False
⊢ False

Tactic:
obtain ⟨i, hio, hiμ⟩ := this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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) μ
⊢ i ∣ orderOf μ

Tactic:
replace hio := Nat.dvd_of_mem_divisors hio
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 μ
rw : ∀ (hnμ : orderOf μ ≠ n) (ho : 0 < orderOf μ) (i : ℕ) (hiμ : IsRoot (cyclotomic i K) μ) (hio : i ∣ orderOf μ), False
⊢ False

Tactic:
rw [IsPrimitiveRoot.not_iff] at hnμ

Premises used: IsPrimitiveRoot.not_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 μ
rw :
  ∀ (hμn : orderOf μ ∣ n) (hnμ : orderOf μ ≠ n) (ho : 0 < orderOf μ) (i : ℕ) (hiμ : IsRoot (cyclotomic i K) μ)
    (hio : i ∣ orderOf μ), False
⊢ False

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one] at hμn

Premises used: orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 μ
⊢ 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μ)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ i ∣ n

Tactic:
have key' : i ∣ n := hio.trans hμn
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
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
⊢ False

Tactic:
rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ

Premises used: Polynomial.dvd_iff_isRoot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ {i, n} ⊆ n.divisors

Tactic:
simpa [Finset.insert_subset_iff, key'] using hnpos.ne'

Premises used: Finset.insert_subset_iff, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ {i, n} ⊆ n.divisors

Tactic:
have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
obtain :
  ∀ (k : K[X]) (hk : cyclotomic i K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * k), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := hiμ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
obtain :
  ∀ (j : K[X]) (hj : cyclotomic n K = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) * j), False
⊢ False

Tactic:
obtain ⟨j, hj⟩ := hμ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ ∏ i ∈ n.divisors, cyclotomic i K = HPow.hPow (α := K[X]) X n - 1

Tactic:
have := prod_cyclotomic_eq_X_pow_sub_one hnpos K
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ (∏ 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

Premises used: Finset.prod_pair, Finset.prod_sdiff, LT.lt.ne
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ Squarefree (HPow.hPow (α := K[X]) X n - 1)

Tactic:
have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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)
⊢ ∀ (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

Premises used: Squarefree
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ (∏ 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)) =
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]) *
      ((∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * k * j)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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
⊢ 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⟩

Premises used: Polynomial.C, HMul.hMul, HSub.hSub, Polynomial.cyclotomic, Insert.insert, Finset.prod, Nat.divisors, SDiff.sdiff, Exists.intro, Singleton.singleton, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
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 : IsUnit (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))
⊢ False

Tactic:
simp [Polynomial.isUnit_iff_degree_eq_zero] at hn

Premises used: Polynomial.isUnit_iff_degree_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) (↑n : R)
μ : R
⊢ Function.Injective (α := R) (β := FractionRing R) (⇑(algebraMap R (FractionRing R)) : (a : R) → FractionRing R)

Tactic:
have hf : Function.Injective _ := IsFractionRing.injective R (FractionRing R)