no goals
α : Type u_1
β : Type ?u.10243
γ : Type ?u.10246
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[Iio ↑n] ↑n) (pure (n - 1))
simpa only [ceil_intCast] using tendsto_floor_left_pure_ceil_sub_one (n : α)