intro k _
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ d then 1 else 0) * (S⁻¹ * ↑(μ d) * if d ∣ x ∧ ↑x ^ 2 ≤ y then g x else 0) =
      if l ∣ d ∧ d ∣ x ∧ ↑x ^ 2 ≤ y then g x * S⁻¹ * ↑(μ d) else 0
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