rw [sum_mul_subst k P, sum_congr rfl]
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    ∑ i ∈ P.divisors, g k * if (↑k * ↑i) ^ 2 ≤ y ∧ i.Coprime d then g i else 0
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ x ∈ P.divisors,
    (if k * x ∣ P then if k = d.gcd (k * x) ∧ ↑(k * x) ^ 2 ≤ y then g (k * x) else 0 else 0) =
      g k * if (↑k * ↑x) ^ 2 ≤ y ∧ x.Coprime d then g x else 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
hkd : k ∣ d
⊢ ∀ (l : ℕ), l ∣ P → ¬k ∣ l → (if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0