no goals
𝓕 : Type ?u.451724
𝕜 : Type ?u.451727
α : Type ?u.451730
ι : Type ?u.451733
κ : Type ?u.451736
E : Type u_1
F : Type ?u.451742
G : Type ?u.451745
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ comap norm (𝓝 0) = 𝓝 1
simpa only [dist_one_right] using nhds_comap_dist (1 : E)