no goals
𝓕 : Type ?u.55420
𝕜 : Type ?u.55423
α : Type ?u.55426
ι : Type ?u.55429
κ : Type ?u.55432
E : Type u_1
F : Type ?u.55438
G : Type ?u.55441
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
⊢ dist b (a * b) = ‖a‖
rw [← dist_one_left, ← dist_mul_right 1 a b, one_mul]