no goals
F : Type ?u.995091
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x✝ : α
C : ℝ
x : α
⊢ ‖↑f x‖ = dist (↑f x) (↑0 x)
simp [dist_zero_right]