feat(Geometry/Euclidean/Angle/Sphere): Add theorem about cospherical points on two intersecting lines

[zcyemi]

---

Add cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi.

This theorem is the converse of EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi.
However, the ambient type is required to be two-dimensional, i.e. Fact (finrank ℝ V = 2).
I don‘t think (not entirely sure) that lifting the ambient space from dimension 2 to arbitrary dimension is reasonable for this theorem, since the proof is entirely carried out in a two-dimensional plane.
Therefore, I place this theorem in Euclidean/Angle/Sphere rather than Euclidean/Sphere/Power.

Deps:

• depends on: [Merged by Bors] - feat(Geometry/Euclidean/Angle/Oriented/Affine): Add oangle sign lemmas for two intersecting lines #33365

[github-actions]

PR summary 61d1f8fbef

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Euclidean.Angle.Sphere	2026	2030	+4 (+0.20%)

Import changes for all files

Files	Import difference
Mathlib.Geometry.Euclidean.Angle.Sphere	4

---

Declarations diff

+ _root_.Sbtw.oangle_sign_eq_of_sbtw
+ _root_.Sbtw.oangle_sign_eq_of_sbtw_left
+ cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jsm28]

I think the result should be proved for an ambient space of arbitrary dimension, without requiring to be given an orientation, since it's true in general without those requirements. Rather, you can move to a two-dimensional subspace and pick an orientation of that subspace within the proof while proving the result more generally. dist_div_sin_angle_div_two_eq_circumradius is an example of an existing proof in mathlib that does just that (moves to a subspace in order to use oriented angles as part of proving a result that doesn't use them in the statement); you can see move examples of such arguments in #32282.

[jsm28]

You might need to add a lemma that says cospherical points in a subspace are cospherical in the larger space (which could be deduced from a more general statement that cospherical points mapped by an isometry are still cospherical), but that should be straightforward to prove.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Geometry/Euclidean/Angle/Oriented/Affine): Add oangle sign lemmas for two intersecting lines #33365
  By Dependent Issues (🤖). Happy coding!