calc
  (∑ l in divisors P, if l ∣ d then g l else 0) =
      ∑ l in divisors P, if l ∣ d then g (d / l) else 0 := by
    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]
  _ = g d * ∑ l in divisors P, if l ∣ d then 1 / g l else 0 := by
    rw [mul_sum]; apply sum_congr rfl; intro l hl
    rw [mul_ite_zero]; apply if_ctx_congr Iff.rfl _ (fun _ => rfl); intro h
    rw [← div_mult_of_dvd_squarefree g s.selbergTerms_mult d l]; ring
    exact h; apply Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree
    apply _root_.ne_of_gt; rw [mem_divisors] at hl ; apply selbergTerms_pos; exact hl.left
  _ = g d * (ν d)⁻¹ := by rw [← s.nu_eq_conv_one_div_selbergTerms d hd]
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g l else 0) = g d * (ν d)⁻¹
no goals