no goals
α : Type u_1
β : Type ?u.269625
γ : Type ?u.269628
ι : Type ?u.269631
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
  mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]