rw [← sum_over_dvd_ite s.prodPrimes_ne_zero hd,
  ← Nat.sum_divisorsAntidiagonal fun x _ => g x, Nat.sum_divisorsAntidiagonal' fun x _ => g x,
  sum_over_dvd_ite s.prodPrimes_ne_zero hd]
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g l else 0) = ∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0
no goals