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