rw [sum_eq_single (l/k)]
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = ∑ m ∈ n.divisors, if l = k * m then f l else 0
case pos
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ f l = if l = k * (l / k) then f l else 0

case pos.h₀
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ ∀ b ∈ n.divisors, b ≠ l / k → (if l = k * b then f l else 0) = 0

case pos.h₁
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
l : ℕ
hl : l ∈ n.divisors
hkl : k ∣ l
⊢ l / k ∉ n.divisors → (if l = k * (l / k) then f l else 0) = 0