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