simp only [Nat.ceil_one, Nat.floor_coe, Finset.mem_filter, Finset.mem_Icc, Finset.mem_range,
  and_congr_left_iff]
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) ↔ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p.Prime → (1 ≤ p ∧ p ≤ n ↔ p < n + 1)