rw [Finset.card_eq_sum_ones, ←Finset.sum_filter, Nat.cast_sum]
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0) =
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support).card
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
⊢ ∑ a ∈ Finset.filter (fun d => s.prodPrimes.Coprime d) s.support, s.weights a =
    ∑ x ∈ Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) s.support, ↑1