Commit 2021-09-26 10:39 a2517af6

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).