no goals
𝓕 : Type ?u.636975
𝕜 : Type ?u.636978
α : Type ?u.636981
ι : Type ?u.636984
κ : Type ?u.636987
E : Type u_1
F : Type ?u.636993
G : Type ?u.636996
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
a b : E
⊢ dist a (a * b) = ‖b‖
rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one]