rw [this d1, this d2]
case neg.h.h
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 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) = 0
case neg.h.h
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 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then 0 * 0 else 0) = 0