mathlib3

7cff8250 - feat(data/vector2): induction principle, define last, and some lemmas (blocked by #4578) (#4554)

feat(data/vector2): induction principle, define last, and some lemmas (blocked by #4578) (#4554) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>