α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
⊢ NeBot (𝓝[{x}ᶜ] x)
rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
rintro ε ε0
case intro.intro
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩
case intro.intro
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε
case intro.intro
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
refine' ⟨x + b, mt (Set.mem_singleton_iff.trans add_right_eq_self).1 <| norm_pos_iff.1 hb0, _⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.375059
γ : Type ?u.375062
ι : Type ?u.375065
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε
rwa [dist_comm, dist_eq_norm, add_sub_cancel']