no goals
𝓕 : Type ?u.63293
𝕜 : Type ?u.63296
α : Type ?u.63299
ι : Type ?u.63302
κ : Type ?u.63305
E : Type u_1
F : Type ?u.63311
G : Type ?u.63314
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
⊢ ‖a * b‖ ≤ ‖a‖ + ‖b‖
simpa [dist_eq_norm_div] using dist_triangle a 1 b⁻¹