no goals
𝓕 : Type ?u.635485
𝕜 : Type ?u.635488
α : Type ?u.635491
ι : Type ?u.635494
κ : Type ?u.635497
E : Type u_1
F : Type ?u.635503
G : Type ?u.635506
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x y : E
⊢ dist x⁻¹ y = dist x y⁻¹
simp_rw [dist_eq_norm_div, ← norm_inv' (x⁻¹ / y), inv_div, div_inv_eq_mul, mul_comm]