mathlib3

a2517af6 - refactor(data/fin,*): redefine `insert_nth`, add lemmas (#9349)

refactor(data/fin,*): redefine `insert_nth`, add lemmas (#9349) ### `data/fin` * add `fin.succ_above_cast_lt`, `fin.succ_above_pred`, `fin.cast_lt_succ_above`, `fin.pred_succ_above`; * add `fin.exists_succ_above_eq` and `fin.exists_succ_above_eq_iff`, use the latter to prove `fin.range_succ_above`; * add `@[simp]` to `fin.succ_above_left_inj`; * add `fin.cases_succ_above` induction principle, redefine `fin.insert_nth` to be `fin.cases_succ_above`; * add lemmas about `fin.insert_nth` and some algebraic operations. ### `data/fintype/basic` * add `finset.insert_compl_self`; * add `fin.image_succ_above_univ`, `fin.image_succ_univ`, `fin.image_cast_succ` and use them to prove `fin.univ_succ`, `fin.univ_cast_succ`, and `fin.univ_succ_above` using `by simp`; ### `data/fintype/card` * slightly golf the proof of `fin.prod_univ_succ_above`; * use `@[to_additive]` to generate some proofs. ### `topology/*` * prove continuity of `fin.insert_nth` in both arguments and add all the standard dot-notation `*.fin_insert_nth` lemmas (`*` is one of `filter.tendsto`, `continuous_at`, `continuous_within_at`, `continuous_on`, `continuous`).