apply lambdaSquared_eq_zero_of_support_wlog hw hd d2 d1 (Nat.lcm_comm d1 d2 ▸ h) hle
case pos.inr
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
h : d = d1.lcm d2
hle : d2 ≤ d1
⊢ w d2 * w d1 = 0
no goals