chore(data/fintype/basic): Better `fin` lemmas (#14200)
Turn `finset.image` into `finset.map` and `insert` into `finset.cons` in the three lemmas relating `univ : finset (fin (n + 1))` and `univ : finset (fin n)`. Golf proofs involving the related big operators lemmas.
