mathlib

91288e35 - feat(data/fin/tuple): rename `fin.append` to `matrix.vec_append`, introduce a new `fin.append` and `fin.repeat`. (#10346)

feat(data/fin/tuple): rename `fin.append` to `matrix.vec_append`, introduce a new `fin.append` and `fin.repeat`. (#10346) We already had `fin.append v w h`, which combines the append operation with casting. This commit removes the `h` argument, allowing it to be defeq to `fin.add_cases`, and moves the previous definition to the name `matrix.vec_append` matching `matrix.vec_cons` and similar. Another advantage of dropping `h` is that it is clearer how to state lemmas like `append_assoc`, as we only have one proof argument to keep track of instead of four. As it turns out, to implement a `gmonoid` structure on tuples (under concatenation), `fin.append` without the `h` argument is all that's needed. We implement `matrix.vec_append` in terms of `fin.append`, but provide a lemma that unfolds it to the old definition so as to avoid having to rewrite all the other proofs. Removing `matrix.vec_append` entirely is left to investigate in some future PR. Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>