no goals
α : Type ?u.69959
β : Type ?u.69962
γ : Type ?u.69965
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ 𝓟 (Icc (⊤ - 1) (⊤ + 1)) ≤ 𝓝 ⊤
simpa only [← coe_one, top_sub_coe, top_add, Icc_self, principal_singleton] using pure_le_nhds _