mathlib

29014241 - feat(linear_algebra/affine_space/midpoint): `midpoint_eq_left_iff`, `midpoint_eq_right_iff` (#17385)

feat(linear_algebra/affine_space/midpoint): `midpoint_eq_left_iff`, `midpoint_eq_right_iff` (#17385) Add two `simp` lemmas `midpoint_eq_left_iff` and `midpoint_eq_right_iff`: the midpoint of two points equals one of those points if and only if the two points are equal. Also add analogous `left_eq_midpoint_iff` and `right_eq_midpoint_iff`.