no goals
𝓕 : Type ?u.646954
𝕜 : Type ?u.646957
α : Type ?u.646960
ι : Type ?u.646963
κ : Type ?u.646966
E : Type u_1
F : Type ?u.646972
G : Type ?u.646975
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 [div_eq_mul_inv, dist_inv_inv] using dist_mul_mul_le a₁ a₂⁻¹ b₁ b₂⁻¹