case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
obtain ⟨hd, hdn⟩ := Nat.mem_properDivisors.mp h
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
h0n : 0 < n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
have h0n : 0 < n := pos_of_gt hdn
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
h0n : 0 < n
h0d : 0 < d
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
h0n : 0 < n
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
have h0d : 0 < d := Nat.pos_of_dvd_of_pos hd h0n
no goals
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ Nat.properDivisors n
hd : d ∣ n
hdn : d < n
h0n : 0 < n
h0d : 0 < d
⊢ (X ^ d - 1) * ∏ x in Nat.divisors n \ Nat.divisors d, cyclotomic x R = X ^ n - 1
rw [← prod_cyclotomic_eq_X_pow_sub_one h0d, ← prod_cyclotomic_eq_X_pow_sub_one h0n, mul_comm,
  Finset.prod_sdiff (Nat.divisors_subset_of_dvd h0n.ne' hd)]