swap
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 neg
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) = 0
case neg
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) = 0

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