no goals
𝓕 : Type ?u.639132
𝕜 : Type ?u.639135
α : Type ?u.639138
ι : Type ?u.639141
κ : Type ?u.639144
E : Type u_1
F : Type ?u.639150
G : Type ?u.639153
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
a b : E
⊢ dist (a * b) a = ‖b‖
rw [dist_comm, dist_self_mul_right]