apply sum_le_sum
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≥
    ∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ ∀ i ∈ P.divisors,
    (if i ∣ d then g i * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) ≤
      if i ∣ d then g i * ∑ m ∈ P.divisors, if (↑i * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0