mathlib3

f2900006 - feat(data/equiv/fin): rename sum_fin_sum_equiv to fin_sum_fin_equiv (#6857)

feat(data/equiv/fin): rename sum_fin_sum_equiv to fin_sum_fin_equiv (#6857) Renames `sum_fin_sum_equiv` to `fin_sum_fin_equiv` (as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/sum_fin_add_comm_equiv)) Introduces a version with `fin(n + m)` instead of `fin(m + n)` Adds a bunch of simp lemmas for applying these (and their inverses)