no goals
𝓕 : Type ?u.329402
𝕜 : Type ?u.329405
α : Type ?u.329408
ι : Type ?u.329411
κ : Type ?u.329414
E : Type u_1
F : Type ?u.329420
G : Type ?u.329423
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x : E
⊢ edist x 1 = ↑‖x‖₊
rw [edist_eq_coe_nnnorm_div, div_one]