rw [selbergWeights_eq_dvds_sum, ← boole_mul, mul_sum, mul_sum]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∑ i ∈ P.divisors, (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ i ∧ ↑i ^ 2 ≤ y then g i else 0) =
    ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0