split_ifs with h h' h'
case h
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
⊢ (if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤ 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
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ g m ≤ g m

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ g m ≤ 0

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
h' : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ 0 ≤ g m

case neg
s : SelbergSieve
d : ℕ
hdP : d ∣ P
k : ℕ
a✝ : k ∈ P.divisors
hkd : k ∣ d
m : ℕ
hm : m ∈ P.divisors
h : ¬((↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
h' : ¬((↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d)
⊢ 0 ≤ 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