rw [apply_ite abs, abs_zero, abs_mul]
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ |if n = d1.lcm d2 then s.selbergWeights d1 * s.selbergWeights d2 else 0| ≤ f d1 d2
case calc_3.h.h
s : SelbergSieve
n : ℕ
hn : n ∈ P.divisors
f : ℕ → ℕ → ℝ := fun x z => if n = x.lcm z then 1 else 0
d1 : ℕ
a✝¹ : d1 ∈ n.divisors
d2 : ℕ
a✝ : d2 ∈ n.divisors
⊢ (if n = d1.lcm d2 then |s.selbergWeights d1| * |s.selbergWeights d2| else 0) ≤ f d1 d2