use ∏ p in m.primeFactors, p
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 : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
⊢ ∃ a, ((a ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑a ^ 2 ≤ s.level) ∧ (m ∣ a ^ ⌊s.level⌋₊ ∧ a ^ ⌊s.level⌋₊ ≠ 0) ∧ a ∣ m

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 : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ 0 ≤ √s.level
case 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 : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
⊢ ((∏ p ∈ m.primeFactors, p ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑(∏ p ∈ m.primeFactors, p) ^ 2 ≤ s.level) ∧
    (m ∣ (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ∧ (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0) ∧
      ∏ p ∈ m.primeFactors, p ∣ m

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 : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ 0 ≤ √s.level