have : ∀ d' : ℕ, w d' = 0 := by
  intro d'; apply hw
  have : (0:ℝ) ≤ (d') ^ 2 := by norm_num
  linarith
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
case neg
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : y < ↑d
hy : y < 0
this : ∀ (d' : ℕ), w d' = 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0