apply mul_le_mul le_rfl _ _ (le_of_lt $ s.selbergTerms_pos k $ Trans.trans hkd hdP)
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    g k * ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ (∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    ∑ m ∈ P.divisors, if (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0