PRs towards IMO geometry 2024 P4

Stream: PR reviews

[Joseph Myers]

I currently have the following 14 PRs open working towards IMO geometry problem 2024 P4 (I expect a fair number more in this series before that formalization is finished).

• The final three PRs on the relation of angle bisection to incenter / excenter: #30477, #30981, #30982
• The interaction of Affine.Simplex.reindex to various other simplex definitions: #31054, #31055, #31056, #31057 (#31210, #31256, #31257 are three more such PRs to complete the set of such lemmas on reindex interaction with other simplex definitions, but aren't on the path to IMO 2024 P4)
• Real.Angle lemma: #30943
• Other affine space lemmas: #31167, #31172, #31204, #31205
• Other incenter / excenter lemmas: #31173, #31206

[Joseph Myers]

After some PRs were merged and others opened, I now have 17 open PRs in this series:

• The final three PRs on the relation of angle bisection to incenter / excenter: #30477, #30981, #30982
• The interaction of Affine.Simplex.reindex to various other simplex definitions: #31054, #31055 (maintainer-merge state), #31056, #31057 (#31210, #31256, #31257 are three more such PRs to complete the set of such lemmas on reindex interaction with other simplex definitions, but aren't on the path to IMO 2024 P4)
• Other affine space lemmas: #31172, #31204, #31205
• Other incenter / excenter lemmas: #31173, #31206, #31493
• Convex combination lemmas: #31451, #31452
• Sphere.secondInter lemmas: #31494, #31495

[Joseph Myers]

The current 13 open PRs in this series:

• The final two PRs setting up the relation of angle bisection to incenter / excenter: #30981, #30982.
• The interaction of Affine.Simplex.reindex to various other simplex definitions: #31054, #31056, #31057 (#31210, #31256 are two more such PRs to complete the set of such lemmas on reindex interaction with other simplex definitions, but aren't on the path to IMO 2024 P4).
• Other affine space lemmas: #31205, #31712.
• Other incenter / excenter lemmas: #31206, #31733.
• Convex combination lemmas in strictly convex sets and spaces: #31452.
• Angle lemmas: #31713.
• Sphere.secondInter lemmas: #31495.
• Tangents / orthRadius lemmas: #31731.

[Joseph Myers]

I'd like to ping the orthRadius lemmas in #31731 early, since I'd like to move orthRadius to a separate file next (in preparation for using it in defining pole and polar) and such a refactoring PR moving existing material is awkward while there are also additions to that existing material under review.

[Joseph Myers]

Thanks for the review! The PR splitting out orthRadius is now #31850; I have the material ready for the next three PRs building on that once it's in.

[Joseph Myers]

This series is now complete (and so formalization of all six IMO 2024 problems is complete). #32295, with 25 open dependencies, has the IMO 2024 P4 formalization itself. Of the 25 open dependencies, the following have no open dependencies themselves and so are ready for review (and merging them will make various of the other dependencies ready for review).

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31205: feat(Analysis/Convex/Side): affine combinations and sides of faces of a simplex
• #31452: feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces
• #31733: feat(Geometry/Euclidean/Incenter): orthRadius lemmas
• #31979: feat(LinearAlgebra/AffineSpace/Independent): injectivity of spans of images
• #32004: feat(Geometry/Euclidean/Angle/Sphere): unoriented law of sines with circumradius
• #32019: feat(Geometry/Euclidean/Projection): map and subtype lemmas
• #32023: feat(Geometry/Euclidean/Sphere/SecondInter): isometry and subtype lemmas
• #32259: feat(Analysis/SpecialFunctions/Trigonometric/Angle): toReal addition lemmas
• #32290: feat(Geometry/Euclidean/Circumcenter): circumcenter_ne_point
• #32296: refactor(LinearAlgebra/FiniteDimensional/Defs): move of_fact_finrank_eq_two

[Joseph Myers]

Thanks for the reviews so far. We're now down to 18 open dependencies, of which the following 8 have no open dependencies themselves and so are ready for review.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31495: feat(Geometry/Euclidean/Sphere/SecondInter): secondInter and sides of faces of a simplex
• #31733: feat(Geometry/Euclidean/Incenter): orthRadius lemmas
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32019: feat(Geometry/Euclidean/Projection): map and subtype lemmas
• #32259: feat(Analysis/SpecialFunctions/Trigonometric/Angle): toReal addition lemmas
• #32273: feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex

Also note that once the full series is in, Mathlib.Geometry.Euclidean.Incenter will be very close to the 1500-line limit, but I propose to wait for all the PRs to that file to be merged before splitting it into three.

[Joseph Myers]

Thanks for the further reviews. We're now at 15 dependencies, with the following 7 immediately available for review as having no further open dependencies themselves.

• #30981: feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection mod π
• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31495: feat(Geometry/Euclidean/Sphere/SecondInter): secondInter and sides of faces of a simplex
• #31891: feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars
• #32021: feat(Geometry/Euclidean/Altitude): map and restrict lemmas
• #32260: feat(Geometry/Euclidean/Angle/Oriented/Affine): oriented angle bisection and halving unoriented angles
• #32273: feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex