rw [← sum_filter, Finset.sum_const, smul_one_eq_cast]
case calc_5
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
⊢ ∑ p ∈ n.divisors ×ˢ n.divisors, f p.1 p.2 = ↑(filter (fun p => n = p.1.lcm p.2) (n.divisors ×ˢ n.divisors)).card
no goals