no goals
α : Type u_1
β : Type ?u.12341
γ : Type ?u.12344
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto ceil (𝓝[Ioi ↑n] ↑n) (pure (n + 1))
simpa only [floor_intCast] using tendsto_ceil_right_pure_floor_add_one (n : α)