intro d1 hd1
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 = x.lcm d2 then w x * w d2 * ν x_1 else 0) =
      ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) =
    ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹