theorem Finset.card_le_card_iff_of_subset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) : t.card ≤ s.card ↔ s = t

theorem Finset.card_lt_card_iff_of_subset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) : s.card < t.card ↔ s ≠ t