no goals
α : Type ?u.11637
R : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})
cases' eq_or_ne ⌈n⌉₊ 0 with h h <;> simp_all [h, Nat.preimage_ceil_of_ne_zero]