apply sum_congr rfl
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
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ x_1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x_1 = x.lcm d2 then weights x * weights d2 else 0) =
      (∑ d ∈ n.divisors, weights d) * weights x