R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
have hdn := (Nat.mem_properDivisors.mp h).2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
use ∏ x in n.properDivisors \ d.divisors, cyclotomic x R
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R
symm
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R =
    (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
convert X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h using 1
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * (cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R) =
    (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R =
    (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
rw [mul_assoc]
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R =
    ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
case h.e'_2
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ (X ^ d - 1) * (cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R) =
    (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
congr 1
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ ¬n ∈ Nat.properDivisors n \ Nat.divisors d

case h.e'_2.e_a.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ ¬n ∈ Nat.divisors d
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ cyclotomic n R * ∏ x in Nat.properDivisors n \ Nat.divisors d, cyclotomic x R =
    ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R
rw [← Nat.insert_self_properDivisors hdn.ne_bot, insert_sdiff_of_not_mem, prod_insert]
no goals
case h.e'_2.e_a
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ ¬n ∈ Nat.properDivisors n \ Nat.divisors d
exact Finset.not_mem_sdiff_of_not_mem_left Nat.properDivisors.not_self_mem
no goals
case h.e'_2.e_a.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hdn : d < n
⊢ ¬n ∈ Nat.divisors d
exact fun hk => hdn.not_le <| Nat.divisor_le hk