rw [prod_factors_sum_pow_compMult (Nat.floor s.level) _ s.nu]
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
hlsq : Squarefree l
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤
    ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n)

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
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.selbergTerms l
case 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ CompletelyMultiplicative s.nu

case hd
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
hlsq : Squarefree l
⊢ Squarefree l

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
hlsq : Squarefree l
⊢ ⌊s.level⌋₊ ≠ 0

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
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.selbergTerms l