apply if_ctx_congr _ _ (fun _ => rfl)
case a
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ (if ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k then ↑(μ d) * g k * S⁻¹ else 0) =
    if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l ∣ d ∧ d ∣ k ↔ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
a✝¹ : k ∈ P.divisors
d : ℕ
a✝ : d ∈ P.divisors
⊢ l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y → ↑(μ d) * g k * S⁻¹ = g k * S⁻¹ * ↑(μ d)