intro k hk
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ x ∈ P.divisors,
    (∑ l ∈ P.divisors, if x = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
      if x ∣ d then g x * ∑ m ∈ P.divisors, if (↑x * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
hk : k ∈ P.divisors
⊢ (∑ l ∈ P.divisors, if k = d.gcd l ∧ ↑l ^ 2 ≤ y then g l else 0) =
    if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0