intro d1 _
case pos.h
s : Sieve
w : ℕ → ℝ
y : ℝ
hw : ∀ (d : ℕ), ¬↑d ^ 2 ≤ y → w d = 0
d : ℕ
hd : ¬↑d ≤ y
hy : 0 ≤ y
⊢ ∀ x ∈ d.divisors, (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) = 0
case pos.h
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 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) = 0