-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic'_eq_X_pow_sub_one_div {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ}
    (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
    cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i ∈ Nat.properDivisors n, cyclotomic' i K

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x 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

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K ∧
    ⊥ < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Tactic:
refine ⟨by rw [mul_comm], ?_⟩

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ ⊥ < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ ⊥ < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Tactic:
rw [bot_lt_iff_ne_bot]

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K).degree ≠ ⊥

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic

Tactic:
apply monic_prod_of_monic

Result:
case hs
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ n.properDivisors, (cyclotomic' i K).Monic

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h✝ : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
h : (∏ i ∈ n.properDivisors, cyclotomic' i K).degree = ⊥
⊢ False

Tactic:
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
rw [(div_modByMonic_unique (cyclotomic' n K) 0 prod_monic _).1]

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K).degree ≠ ⊥

Tactic:
intro h

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h✝ : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
h : (∏ i ∈ n.properDivisors, cyclotomic' i K).degree = ⊥
⊢ False

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Tactic:
simp only [degree_zero, zero_add]

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K ∧
    ⊥ < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (X ^ n - 1) /ₘ ∏ 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]

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Proof state:
case hs
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ n.properDivisors, (cyclotomic' i K).Monic

Tactic:
intro i _

Result:
case hs
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
a✝ : i ∈ n.properDivisors
⊢ (cyclotomic' i K).Monic

Proof state:
case hs
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
a✝ : i ∈ n.properDivisors
⊢ (cyclotomic' i K).Monic

Tactic:
exact cyclotomic'.monic i K

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
    cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
rw [mul_comm]

Result:
no goals