intro d1 _
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ d.divisors,
    (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) * ν d =
      ∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 * ν d else 0
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0