mathlib3

d963213b - refactor(algebra/add_torsor,linear_algebra/affine_space/basic): vsub_set (#3858)

refactor(algebra/add_torsor,linear_algebra/affine_space/basic): vsub_set (#3858) The definition of `vsub_set` in `algebra/add_torsor` does something similar to `set.image2`, but expressed directly with `∃` inside `{...}`. Various lemmas in `linear_algebra/affine_space/basic` likewise express such sets of subtractions with a given point on one side directly rather than using `set.image`. These direct forms can be inconvenient to use with lemmas about `set.image2`, `set.image` and `set.range`; in particular, they have the equality inside the binders expressed the other way round, leading to constructs such as `conv_lhs { congr, congr, funext, conv { congr, funext, rw eq_comm } }` when it's necessary to convert one form to the other. The form of `vsub_set` was suggested in review of #2720, the original `add_torsor` addition, based on what was then used in `algebra/pointwise`. Since then, `image2` has been added to mathlib and `algebra/pointwise` now uses `image2`. Thus, convert these definitions to using `image2` or `''` as appropriate, so simplifying various proofs. This PR deliberately only addresses `vsub_set` and related definitions for such sets of subtractions; it does not attempt to change any other definitions in `linear_algebra/affine_space/basic` that might also be able to use `image2` or `''` but are not such sets of subtractions, and does not change the formulations of lemmas not involving such sets even if a rearrangement of equalities and existential quantifiers in some such lemmas might bring them closer to the formulations about images of sets.