feat(geometry/euclidean): Monge point and orthocenter (#3872)
feat(geometry/euclidean): Monge point and orthocenter (#3872)

The main purpose of this PR is to define the orthocenter of a
triangle.

Simplices in more than two dimensions do not in general have an
orthocenter: the altitudes are not necessarily concurrent.  However,
there is a n-dimensional generalization of the orthocenter in the form
of the Monge point of a simplex.  Define a Monge plane to be an
(n-1)-dimensional subspace that passes through the centroid of an
(n-2)-dimensional face of the simplex and is orthogonal to the
opposite edge.  Then the Monge planes of a simplex are always
concurrent, and their point of concurrence is known as the Monge point
of the simplex.  Furthermore, the circumcenter O, centroid G and Monge
point M are collinear in that order on the Euler line, with OG : GM =
(n-1) : 2.

Here, we use that ratio as a convenient way to define the Monge point
in terms of the existing definitions of the circumcenter and the
centroid.  First we set up some infrastructure for dealing with affine
combinations of the vertices of a simplex together with its
circumcenter, which can be convenient for computations rather than
dealing with combinations of the vertices alone; the use of an
inductive type `points_with_circumcenter_index` seemed to be more
convenient than other options for how to index such combinations.
Then, a straightforward calculation using `inner_weighted_vsub` shows
that the point defined in terms of the circumcenter and the centroid
does indeed lie in the Monge planes, so justifying the definition as
being a definition of the Monge point.  It is then shown to be the
only point in that intersection (in fact, the only point in the
intersection of all the Monge planes where one of the two vertices
needed to specify a Monge plane is fixed).

The altitudes of a simplex are then defined.  In the case of a
triangle, the orthocenter is defined to be the Monge point, the
altitudes are shown to equal the Monge planes (mathematically trivial,
but involves quite a bit of fiddling around with `fin 3`) and thus the
orthocenter is shown to lie in the altitudes and to be the unique
point lying in any two of them (again, involves various fiddling
around with `fin 3` to link up with the previous lemmas).  Because of
the definition chosen for the Monge point, the position of the
orthocenter on the Euler line of the triangle comes for free (not
quite `rfl`, but two rewrites of `rfl` lemmas plus `norm_num`).






leanprover-community/mathlib,leanprover-community/mathlib