rw [Finset.mem_filter, Nat.mem_divisors] at hl
case calc_1.h
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
l : ℕ
hl : l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
case calc_1.h
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l