rw [Finset.mem_Icc] at hm
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m