Commit 2022-06-09 01:54 4fc35392

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.