rw [Aux.moebius_inv_dvd_lower_bound_real s.prodPrimes_squarefree l _ (dvd_of_mem_divisors hk),
  ←ite_and, ite_zero_mul, ite_zero_mul, ← ite_and]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : 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 k = l then if ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0 else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l = k then ↑(μ l) * g k * S⁻¹ else 0) = if k = l ∧ ↑l ^ 2 ≤ y then g l * ↑(μ l) * S⁻¹ else 0