intro m _
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
⊢ ∀ x ∈ n.divisors, (∑ x_1 ∈ n.divisors, if x_1 = k * x then f x_1 else 0) = if k * x ∣ n then f (k * x) else 0
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
⊢ (∑ x ∈ n.divisors, if x = k * m then f x else 0) = if k * m ∣ n then f (k * m) else 0