no goals
𝓕 : Type ?u.457116
𝕜 : Type ?u.457119
α : Type ?u.457122
ι : Type ?u.457125
κ : Type ?u.457128
E : Type u_1
F : Type ?u.457134
G : Type ?u.457137
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‖)
simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)