rw [sq, mul_sum, conv_lambda_sq_larger_sum _ n, sum_comm]
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ (∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0) =
    ∑ i ∈ n.divisors, (∑ d ∈ n.divisors, weights d) * weights i