Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.left.left
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

case h.left.right
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) ^ 2 ≤ s.level

case h.right
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
⊢ (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
Tactic:
constructor
Proof state after:
case h.left.left.left
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

case h.left.left.right
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
⊢ s.prodPrimes ≠ 0

case h.left.right
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) ^ 2 ≤ s.level

case h.right
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
⊢ (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