no goals
𝓕 : Type ?u.328683
𝕜 : Type ?u.328686
α : Type ?u.328689
ι : Type ?u.328692
κ : Type ?u.328695
E : Type u_1
F : Type ?u.328701
G : Type ?u.328704
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
a b : E
⊢ edist a b = ↑‖a / b‖₊
rw [edist_dist, dist_eq_norm_div, ofReal_norm_eq_coe_nnnorm']