apply if_ctx_congr _ _ fun _ => rfl
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
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
k : ℕ
hk : k ∈ P.divisors
⊢ ↑k ^ 2 ≤ y ∧ l = k ↔ k = l ∧ ↑l ^ 2 ≤ y

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