rw [sum_comm, sum_congr rfl]
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) =
    ∑ k ∈ P.divisors, ∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors, (if ↑x ^ 2 ≤ y then g x else 0) = ∑ x_1 ∈ P.divisors, if x_1 = d.gcd x ∧ ↑x ^ 2 ≤ y then g x else 0