no goals
𝓕 : Type ?u.49802
𝕜 : Type ?u.49805
α : Type ?u.49808
ι : Type ?u.49811
κ : Type ?u.49814
E : Type u_1
F : Type ?u.49820
G : Type ?u.49823
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ dist a 1 = ‖a‖
rw [dist_eq_norm_div, div_one]