no goals
𝓕 : Type ?u.649048
𝕜 : Type ?u.649051
α : Type ?u.649054
ι : Type ?u.649057
κ : Type ?u.649060
E : Type u_1
F : Type ?u.649066
G : Type ?u.649069
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁✝ a₂✝ b b₁✝ b₂✝ : E
r r₁ r₂ : ℝ
a₁ a₂ b₁ b₂ : E
⊢ abs (dist a₁ b₁ - dist a₂ b₂) ≤ dist (a₁ * a₂) (b₁ * b₂)
simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using
  abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)