apply Finset.sum_le_sum_of_subset_of_nonneg
case calc_2
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
⊢ ∑
      x ∈
        (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
          Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors,
      s.nu x ≥
    ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

case calc_2
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
⊢ (↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)).PairwiseDisjoint fun l =>
    Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
case calc_2.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
⊢ Finset.Icc 1 ⌊√s.level⌋₊ ⊆
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors

case calc_2.hf
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
⊢ ∀
    i ∈
      (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
        Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors,
    i ∉ Finset.Icc 1 ⌊√s.level⌋₊ → 0 ≤ s.nu i

case calc_2
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
⊢ (↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)).PairwiseDisjoint fun l =>
    Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors