mathlib3

f23205e9 - feat(data/vector/basic): make the recursor work with `induction _ using` syntax (#15383)

feat(data/vector/basic): make the recursor work with `induction _ using` syntax (#15383) The `induction` tactic is picky about the order of its arguments, especially when the motive is dependently-typed. Attempting to use `induction v using vector.induction_on` gives the error: > invalid user defined recursor, type of the major premise 'v' does not contain the recursor index 'C' which indicates that the argument order has confused Lean into thinking that the motive is an index. The cause here was that the motive `C` was between the indices (`n`) and the major premise (`v`).