Commit 2022-06-08 07:33 e39af181

chore(data/finset): remove duplicated lemma (#14607) The lemma ssubset_iff_exists_insert_subset was added in #11248 but is just a duplicate of the ssubset_iff lemma a few lines earlier in the file. It's only used once.