trans (∑ d in divisors P, ∑ d1 in divisors d, ∑ d2 in divisors d,
        if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

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