no goals
α : Type ?u.528297
β : Type ?u.528300
ι : Type ?u.528303
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ Tendsto (fun x => ↑⌈x⌉₊ / x) atTop (𝓝 1)
simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)