no goals
α : Type ?u.6253
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 (floor ⁻¹' {⌊n⌋₊})
cases' eq_or_ne ⌊n⌋₊ 0 with h h <;> simp_all [h, Nat.preimage_floor_of_ne_zero]