rw [←Finset.sum_biUnion]
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
⊢ ∑ 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 ≥
    ∑ 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
⊢ ∑
      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