fix: recover convert proof in Geometry.Euclidean.Inversion (#4421)

During porting a `convert` proof was converted to `calc`. This switches to a more direct translation of the original.

We need `using` now because `convert` is happy to descend into the expressions and equate `(HMul.hMul : ℝ → ℝ → ℝ) = (HDiv.hDiv : ℝ → ℝ → ℝ)` since these involve the same types. The old `convert` wouldn't do this because it used simp's congr lemmas, and these require that the functions be defeq rather than just equal.

Mathlib/Geometry/Euclidean/Inversion.lean

@@ -134,10 +134,7 @@ theorem mul_dist_le_mul_dist_add_mul_dist (a b c d : P) :
     dist_inversion_inversion hc hd, one_pow] at H
   rw [← dist_pos] at hb hc hd
   rw [← div_le_div_right (mul_pos hb (mul_pos hc hd))]
-  calc
-    _ = _ := by field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]; ring
-    _ ≤ _ := H
-    _ = _ := by field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]; ring
+  convert H using 1 <;> (field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]; ring)
 #align euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist
 
 end EuclideanGeometry