Unoriented version of the circumcircle angle theorem

Stream: mathlib4

[Jeremy Tan]

While we have the oriented version of this lemma in mathlib, we don't have the unoriented one:

import Mathlib.Geometry.Euclidean.Altitude
import Mathlib.Geometry.Euclidean.Angle.Sphere
import Mathlib.Geometry.Euclidean.Simplex
import Mathlib.Geometry.Euclidean.Sphere.SecondInter

open Affine EuclideanGeometry
open scoped Real

variable {V X : Type*}
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X]

lemma yyy {ABC : Triangle ℝ X} (hA : ∠ (ABC.points 2) (ABC.points 0) (ABC.points 1) ≤ π / 2) :
    ∠ (ABC.points 2) ABC.circumcenter (ABC.points 1) =
    2 * ∠ (ABC.points 2) (ABC.points 0) (ABC.points 1) := by
  sorry

How can this be proved?

[Joseph Myers]

Start by adding lemmas to transfer circumsphere, circumcenter and circumradius across isometries, and in particular across the coercion from an affine subspace to the full space. (We already have those for unoriented angles: AffineIsometry.angle_map and AffineSubspace.angle_coe. But lots of geometrical definitions don't have such lemmas at present.) Then you can move to a two-dimensional subspace spanned by the three points, choose an arbitrary orientation, and use the oriented angle result to deduce the unoriented angle one via existing lemmas relating oriented and unoriented angles. (To use this technique for some results you may also need to use lemmas showing that certain pairs of oriented angles have the same sign; we have plenty of those as well.)

(In principle the lemmas to transfer across isometries could actually apply to any DilationClass, when transferring circumcenter, while circumradius would scale by the ratio of a dilation. But things could probably be done initially for the AffineIsometry and coercion cases and generalized later to cover dilations.)

[Joseph Myers]

This probably also needs a def for mapping a Simplex under an injective affine map, from which the particular case of mapping it from a subspace to the full space can be constructed.

[Joseph Myers]

Probably a tactic could be written to automate "move to a two-dimensional subspace and pick an orientation", once all the relevant lemmas are present, but I expect lots of such proofs need to be written manually before it's clear exactly what such a tactic should look like.

[Eric Wieser]

Joseph Myers said:

This probably also needs a def for mapping a Simplex under an injective affine map, from which the particular case of mapping it from a subspace to the full space can be constructed.

#25156

[Eric Wieser]

#25172 adds the restriction of a simplex to a subspace