no goals
𝓕 : Type ?u.72975
𝕜 : Type ?u.72978
α : Type ?u.72981
ι : Type ?u.72984
κ : Type ?u.72987
E : Type u_1
F : Type ?u.72993
G : Type ?u.72996
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ ‖1‖ = 0
rw [← dist_one_right, dist_self]