apply s.selberg_bound_muPlus d hd
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| ≤ 3 ^ ω d

s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ 0 ≤ 3