mathlib3

8ff139a0 - feat(data/equiv/fin): fin_sum_fin_equiv simp lemmas (#9001)