have hprod_ne_zero :  (∏ p in m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0 := by
  apply pow_ne_zero; apply ne_of_gt; apply hprod_pos
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
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
⊢ m ∈
    (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.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
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors