Theorem: Sieve.boundingSum_ge_sum (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
trans ∑ m in Finset.Icc 1 (Nat.floor $ Real.sqrt s.level), (ζ : ArithmeticFunction ℝ).pdiv .id m
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
rw[←hnu]
State after:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
apply selbergBoundingSum_ge_sum_div
State after:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes

case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative s.nu

case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (n : ℕ), 0 ≤ s.nu n

case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
Tactic:
apply le_of_eq
State after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m = ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m

State before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m = ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Tactic:
apply Finset.sum_congr rfl
State after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑x = ((↑ζ).pdiv ↑ArithmeticFunction.id) x

State before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ x ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑x = ((↑ζ).pdiv ↑ArithmeticFunction.id) x
Tactic:
intro m hm
State after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m

State before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Tactic:
rw [Finset.mem_Icc] at hm
State after:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m

State before:
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
Tactic:
simp only [one_div, ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
  ArithmeticFunction.zeta_apply_ne (show m ≠ 0 by omega), Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
  ArithmeticFunction.id_apply]
State after:
no goals

State before:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
Tactic:
intro p hpp hple
State after:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
hple : ↑p ≤ s.level
⊢ p ∣ s.prodPrimes

State before:
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
hple : ↑p ≤ s.level
⊢ p ∣ s.prodPrimes
Tactic:
apply hP p hpp hple
State after:
no goals

State before:
case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative s.nu
Tactic:
rw[hnu]
State after:
case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative ((↑ζ).pdiv ↑ArithmeticFunction.id)

State before:
case hnu
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ CompletelyMultiplicative ((↑ζ).pdiv ↑ArithmeticFunction.id)
Tactic:
exact CompletelyMultiplicative.zeta.pdiv CompletelyMultiplicative.id
State after:
no goals

State before:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (n : ℕ), 0 ≤ s.nu n
Tactic:
intro n
State after:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ s.nu n

State before:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ s.nu n
Tactic:
rw[hnu]
State after:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ((↑ζ).pdiv ↑ArithmeticFunction.id) n

State before:
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ((↑ζ).pdiv ↑ArithmeticFunction.id) n
Tactic:
apply div_nonneg
State after:
case hnu_nonneg.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ζ n

case hnu_nonneg.hb
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ArithmeticFunction.id n

State before:
case hnu_nonneg.hb
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ArithmeticFunction.id n
Tactic:
simp
State after:
no goals

State before:
case hnu_nonneg.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ↑ζ n
Tactic:
by_cases h : n = 0 <;> simp[h]
State after:
no goals

State before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
Tactic:
intro p hpp _
State after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ s.nu p < 1

State before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ s.nu p < 1
Tactic:
rw[hnu]
State after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ((↑ζ).pdiv ↑ArithmeticFunction.id) p < 1

State before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ((↑ζ).pdiv ↑ArithmeticFunction.id) p < 1
Tactic:
simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
  ArithmeticFunction.zeta_apply, Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
  ArithmeticFunction.id_apply]
State after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (if p = 0 then 0 else 1) / ↑p < 1

State before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (if p = 0 then 0 else 1) / ↑p < 1
Tactic:
rw [if_neg, one_div]
State after:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (↑p)⁻¹ < 1

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0

State before:
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ (↑p)⁻¹ < 1

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
apply inv_lt_one
State after:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < ↑p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0

State before:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < ↑p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
norm_cast
State after:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0

State before:
case hnu_lt.ha
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ 1 < p

case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
exact hpp.one_lt
State after:
case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0

State before:
case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
Tactic:
exact hpp.ne_zero
State after:
no goals

State before:
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ m ≠ 0
Tactic:
omega
State after:
no goals