rw [mul_ite_zero, ite_zero_mul_ite_zero]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ k ∧ ↑k ^ 2 ≤ y then g k else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝¹ : d ∈ P.divisors
k : ℕ
a✝ : k ∈ P.divisors
⊢ (if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then 1 * (S⁻¹ * ↑(μ d) * g k) else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0