rw [←Aux.sum_intro]
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (∑ x ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0) = weights d2 * weights d1
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ weights d1 * weights d2 = weights d2 * weights d1

case hd
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors