mathlib3

df1e6f92 - refactor(data/{finset,multiset}): move inductions proofs on sum/prod from finset to multiset, add more induction lemmas (#6561)

refactor(data/{finset,multiset}): move inductions proofs on sum/prod from finset to multiset, add more induction lemmas (#6561) The starting point is `finset.le_sum_of_subadditive`, which is extended in several ways: * It is written in multiplicative form, and a `[to_additive]` attribute generates the additive version, * It is proven for multiset, which is then used for the proof of the finset case. * For multiset, some lemmas are written for foldr/foldl (and prod is a foldr). * Versions of these lemmas specialized to nonempty sets are provided. These don't need the initial hypothesis `f 1 = 1`/`f 0 = 0`. * The new `..._on_pred` lemmas like `finset.le_sum_of_subadditive_on_pred` apply to functions that are only sub-additive for arguments that verify some property. I included an application of this with `snorm_sum_le`, which uses that the Lp seminorm is subadditive on a.e.-measurable functions. Those `on_pred` lemmas could be avoided by constructing the submonoid given by the predicate, then using the standard subadditive result, but I find convenient to be able to use them directly. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>