-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ}
    (h : d ∈ n.properDivisors) : (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R =
    (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R

Tactic:
rw [mul_assoc]

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * (cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R) =
    (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R

Proof state:
case h.e'_2.e_a.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ n ∉ d.divisors

Tactic:
exact fun hk => hdn.not_le <| Nat.divisor_le hk

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
convert X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h using 1

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R =
    (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R

Proof state:
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ n ∉ n.properDivisors \ d.divisors

Tactic:
exact Finset.not_mem_sdiff_of_not_mem_left Nat.properDivisors.not_self_mem

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Tactic:
symm

Result:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = X ^ n - 1

Proof state:
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R

Tactic:
rw [← Nat.insert_self_properDivisors hdn.ne_bot, insert_sdiff_of_not_mem, prod_insert]

Result:
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ n ∉ n.properDivisors \ d.divisors

case h.e'_2.e_a.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ n ∉ d.divisors

Proof state:
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1

Tactic:
use ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Result:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * (cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R) =
    (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R

Tactic:
congr 1

Result:
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R

Proof state:
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1

Tactic:
have hdn := (Nat.mem_properDivisors.mp h).2

Result:
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1