Criterion for `set.finite` from finsets

Stream: Is there code for X?

[Heather Macbeth]

Looking for this lemma, or a slick proof!

import data.set.finite

example {β : Type*} {n : ℕ} (H : ∀ (s : finset β), s.card ≤ n) :
  (set.univ : set β).finite :=
sorry

[Adam Topaz]

import data.set.finite

example {β : Type*} {n : ℕ} (H : ∀ (s : finset β), s.card ≤ n) :
  (set.univ : set β).finite :=
begin
  haveI : fintype β := fintype_of_finset_card_le n H,
  exact set.finite_univ
end

[Heather Macbeth]

Nice, thanks!