no goals
𝓕 : Type ?u.60638
𝕜 : Type ?u.60641
α : Type ?u.60644
ι : Type ?u.60647
κ : Type ?u.60650
E : Type u_1
F : Type ?u.60656
G : Type ?u.60659
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
a b c : E
⊢ dist a (b / c) = dist (a * c) b
rw [← dist_mul_right _ _ c, div_mul_cancel']