mathlib3

20d6b6a7 - chore(*): add more simp lemmas, refactor theorems about `fintype.sum` (#5888)

chore(*): add more simp lemmas, refactor theorems about `fintype.sum` (#5888) * `finset.prod_sum_elim`, `finset.sum_sum_elim`: use `finset.map` instead of `finset.image`; * add `multilinear_map.coe_mk_continuous`, `finset.order_emb_of_fin_mem`, `fintype.univ_sum_type`, `fintype.prod_sum_elim`, `sum.update_elim_inl`, `sum.update_elim_inr`, `sum.update_inl_comp_inl`, `sum.update_inl_comp_inr`, `sum.update_inr_comp_inl`, `sum.update_inr_comp_inr` and `apply` versions of `sum.*_comp_*` lemmas, * move some lemmas about `function.update` from `data.set.function` to `logic.function.basic`; * rename `sum.elim_injective` to `function.injective.sum_elim` * `simps` lemmas for `function.embedding.inl` and `function.embedding.inr`; * for `e : α ≃o β`, simplify `e.to_equiv.symm` to `e.symm_to_equiv`; * add `continuous_multilinear_map.to_multilinear_map_add`, `continuous_multilinear_map.to_multilinear_map_smul`, and `simps` for `continuous_multilinear_map.to_multilinear_map_linear`.