α : Type u_1
β : Type ?u.16071
γ : Type ?u.16074
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[Iic ↑(n - 1)] ↑(n - 1)
α : Type u_1
β : Type ?u.16071
γ : Type ?u.16074
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[Iic (↑n - 1)] (↑n - 1)
rw [← @cast_one α, ← cast_sub]
no goals
α : Type u_1
β : Type ?u.16071
γ : Type ?u.16074
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[Iic ↑(n - 1)] ↑(n - 1)
exact pure_le_nhdsWithin le_rfl