feat(Geometry/Euclidean/Sphere/SecondInter): add secondInter difference lemmas (#42308)

This PR adds formulas for the difference and distance between the values of
  `Sphere.secondInter` associated with two sphere centers and a common base point
  and direction.

  The general statements do not require the direction to have norm one. Convenient
  unit-direction corollaries are provided as well:

  - `Sphere.secondInter_vsub_secondInter`
  - `Sphere.secondInter_vsub_secondInter_of_norm_eq_one`
  - `Sphere.dist_secondInter_secondInter`
  - `Sphere.dist_secondInter_secondInter_of_norm_eq_one`

  The results describe how the second intersection changes when the sphere center
  is changed, and provide both vector-valued and distance formulations.

Co-authored-by: Scarlett-le <735979178@qq.com>

Author: Scarlett-le

Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean

@@ -144,6 +144,37 @@ theorem Sphere.secondInter_secondInter (s : Sphere P) (p : P) (v : V) :
   convert! zero_div (G₀ := ℝ) _
   ring
 
+/-- The difference between the second intersections of two spheres along a common
+direction `v` is `(2 * ⟪v, s₁.center -ᵥ s₂.center⟫ / ⟪v, v⟫) • v`. -/
+theorem Sphere.secondInter_vsub_secondInter (s₁ s₂ : Sphere P) (p : P) (v : V) :
+    s₁.secondInter p v -ᵥ s₂.secondInter p v = (2 * ⟪v, s₁.center -ᵥ s₂.center⟫ / ⟪v, v⟫) • v := by
+  rw [Sphere.secondInter, Sphere.secondInter, vadd_vsub_vadd_cancel_right, ← sub_smul,
+    ← vsub_sub_vsub_cancel_left s₁.center s₂.center p, inner_sub_right]
+  grind
+
+/-- The difference between the second intersections of two spheres along a common
+unit direction `v` is `(2 * ⟪v, s₁.center -ᵥ s₂.center⟫) • v`. -/
+theorem Sphere.secondInter_vsub_secondInter_of_norm_eq_one (s₁ s₂ : Sphere P) (p : P) {v : V}
+    (hv : ‖v‖ = 1) :
+    s₁.secondInter p v -ᵥ s₂.secondInter p v = (2 * ⟪v, s₁.center -ᵥ s₂.center⟫) • v := by
+  simp [hv, secondInter_vsub_secondInter]
+
+/-- The distance between the second intersections of two spheres along a common
+direction `v` is `2 * |⟪v, s₁.center -ᵥ s₂.center⟫| / ‖v‖`. -/
+theorem Sphere.dist_secondInter_secondInter (s₁ s₂ : Sphere P) (p : P) (v : V) :
+    dist (s₁.secondInter p v) (s₂.secondInter p v) = 2 * |⟪v, s₁.center -ᵥ s₂.center⟫| / ‖v‖ := by
+  rcases eq_or_ne v 0 with rfl | hv
+  · simp
+  simp [dist_eq_norm_vsub, secondInter_vsub_secondInter, norm_smul]
+  grind
+
+/-- The distance between the second intersections of two spheres along a common
+unit direction `v` is `2 * |⟪v, s₁.center -ᵥ s₂.center⟫|`. -/
+theorem Sphere.dist_secondInter_secondInter_of_norm_eq_one (s₁ s₂ : Sphere P) (p : P) {v : V}
+    (hv : ‖v‖ = 1) :
+    dist (s₁.secondInter p v) (s₂.secondInter p v) = 2 * |⟪v, s₁.center -ᵥ s₂.center⟫| := by
+  rw [dist_secondInter_secondInter, hv, div_one]
+
 /-- If the vector passed to `secondInter` is given by a subtraction involving the point in
 `secondInter`, the result of `secondInter` may be expressed using `lineMap`. -/
 theorem Sphere.secondInter_eq_lineMap (s : Sphere P) (p p' : P) :