no goals
α : Type u_1
β : Type ?u.47280
γ : Type ?u.47283
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ
rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]