intro d2 _
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹ =
      ∑ l ∈ P.divisors, if l ∣ d1.gcd x then 1 / g l * (ν d1 * w d1) * (ν x * w x) else 0
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝ : d2 ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0