Commit 2020-08-19 13:32 d963213b

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.