apply lambdaSquared_eq_zero_of_support_wlog hw hd d1 d2 h hle
case pos.inl
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 : d1 ≤ d2
⊢ w d1 * w d2 = 0
no goals