mathlib

b01ca810 - feat(data/matrix/notation): simp lemmas for constant-indexed elements (#4491)

feat(data/matrix/notation): simp lemmas for constant-indexed elements (#4491) If you use the `![]` vector notation to define a vector, then `simp` can extract elements `0` and `1` from that vector, but not element `2` or subsequent elements. (This shows up in particular in geometry if defining a triangle with a concrete vector of vertices and then subsequently doing things that need to extract a particular vertex.) Add `bit0` and `bit1` `simp` lemmas to allow any element indexed by a numeral to be extracted (even when the numeral is larger than the length of the list, such numerals in `fin n` being interpreted mod `n`). This ends up quite long; `bit0` and `bit1` semantics mean extracting alternate elements of the vector in a way that can wrap around to the start of the vector when the numeral is `n` or larger, so the lemmas need to deal with constructing such a vector of alternate elements. As I've implemented it, some definitions also need an extra hypothesis as an argument to control definitional equalities for the vector lengths, to avoid problems with non-defeq types when stating subsequent lemmas. However, even the example added to `test/matrix.lean` of extracting element `123456789` of a 5-element vector is processed quite quickly, so this seems efficient enough. Note also that there are two `@[simp]` lemmas whose proofs are just `by simp`, but that are in fact needed for `simp` to complete extracting some elements and that the `simp` linter does not (at least when used with `#lint` for this single file) complain about. I'm not sure what's going on there, since I didn't think a lemma that `simp` can prove should normally need to be marked as `@[simp]`.