mathlib3

ddbdfeb5 - chore(data/fin): succ_above defn compares fin terms instead of values (#3999)

chore(data/fin): succ_above defn compares fin terms instead of values (#3999) `fin.succ_above` is redefined to use a comparison between two `fin (n + 1)` instead of their coerced values in `nat`. This should delay any "escape" from `fin` into `nat` until necessary. Lemmas are added regarding `fin.succ_above`. Some proofs for existing lemmas reworked for new definition and simplified. Additionally, docstrings are added for related lemmas. New lemmas: Comparison after embedding: `succ_above_lt_ge` `succ_above_lt_gt` Injectivity lemmas: `succ_above_right_inj` `succ_above_right_injective` `succ_above_left_inj` `succ_above_left_injective` finset lemma: `fin.univ_succ_above` prod and sum lemmas: `fin.prod_univ_succ_above` Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>