mathlib3

75351039 - feat(geometry/euclidean/angle/oriented/affine): midpoint lemmas (#17444)

feat(geometry/euclidean/angle/oriented/affine): midpoint lemmas (#17444) Add the lemma that `∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃` and three other similar `simp` lemmas.