no goals
𝓕 : Type ?u.86827
𝕜 : Type ?u.86830
α : Type ?u.86833
ι : Type ?u.86836
κ : Type ?u.86839
E : Type u_1
F : Type ?u.86845
G : Type ?u.86848
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖u‖ = ‖u * v / v‖
rw [mul_div_cancel'']