theorem Finset.ssubset_of_subset_lt_card {α : Type u_1} {s t : Finset α} (h_subset : s ⊆ t) (h_card_le : s.card < t.card) : s ⊂ t

theorem Finset.eq_card_of_eq {α : Type u_1} {s t : Finset α} (h : s = t) : s.card = t.card

theorem Finset.sum_le_card {α : Type u_1} {s : Finset α} {n : ℕ} {f : α → ℕ} (hf : ∀ a ∈ s, f a ≤ n) : ∑ a ∈ s, f a ≤ s.card * n