rw [Aux.sum_intro (f:=fun _ => if l^2 ≤ y then g l * μ l * S⁻¹ else 0) (divisors P) l hl]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0) =
    ∑ k ∈ P.divisors, if k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0