Commit 2021-12-22 18:48 12ee59fa

feat(data/{finset,multiset}/locally_finite): When an Icc is a singleton, cardinality generalization (#10925) This proves Icc a b = {c} ↔ a = c ∧ b = c for sets and finsets, gets rid of the a ≤ b assumption in card_Ico_eq_card_Icc_sub_one and friends and proves them for multisets.