apply Nat.le_floor
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p ≤ ⌊z⌋₊

case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime
case hP.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ ↑p ≤ z

case hP.hp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
p : ℕ
hpp : p.Prime
hp : ↑p ≤ (primeInterSieve x y z hz).level
⊢ p.Prime