no goals
𝓕 : Type ?u.57650
𝕜 : Type ?u.57653
α : Type ?u.57656
ι : Type ?u.57659
κ : Type ?u.57662
E : Type u_1
F : Type ?u.57668
G : Type ?u.57671
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 (a * b) b = ‖a‖
rw [dist_comm, dist_mul_self_right]