rw [← Finset.sum_product']
case calc_4
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, f d1 d2 = ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2
no goals