no goals
𝓕 : Type ?u.641456
𝕜 : Type ?u.641459
α : Type ?u.641462
ι : Type ?u.641465
κ : Type ?u.641468
E : Type u_1
F : Type ?u.641474
G : Type ?u.641477
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
simpa only [dist_mul_left, dist_mul_right] using dist_triangle (a₁ * a₂) (b₁ * a₂) (b₁ * b₂)