trans ↑(Nat.floor z)
case h.a.mpr.right
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑p ≤ z
s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑p ≤ ↑⌊z⌋₊

s : SelbergSieve
hw : ∀ i ∈ s.support, s.weights i = 1
z : ℝ
hz : 1 ≤ z
hP : s.prodPrimes = primorial ⌊z⌋₊
d : ℕ
h : d ∈ s.support ∧ ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d
p : ℕ
hp : p.Prime
hpy : p ≤ ⌊z⌋₊
⊢ ↑⌊z⌋₊ ≤ z