split_ifs with h
case h
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
case pos
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 3 ^ ω d * |s.rem d|

case neg
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
h : ¬↑d ≤ y
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ 0