no goals
𝓕 : Type ?u.454837
𝕜 : Type ?u.454840
α : Type ?u.454843
ι : Type ?u.454846
κ : Type ?u.454849
E : Type u_1
F : Type ?u.454855
G : Type ?u.454858
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x : E
⊢ Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0)
simpa [dist_eq_norm_div] using
  tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)