mathlib3

4fc35392 - refactor(data/finset/nat_antidiagonal): state lemmas with cons instead of insert (#14533)

refactor(data/finset/nat_antidiagonal): state lemmas with cons instead of insert (#14533) This puts less of a burden on the caller rewriting in the forward direction, as they don't have to prove obvious things about membership when evaluating sums. Since this adds the missing `finset.map_cons`, a number of uses of `multiset.map_cons` now need qualified names.