α : Type u_1
β : Type ?u.8142
γ : Type ?u.8145
inst✝ : Fintype α
⊢ card univ = Fintype.card α
α : Type u_1
β : Type ?u.8142
γ : Type ?u.8145
inst✝ : Fintype α
s : Finset α
⊢ s = univ → card s = Fintype.card α
rintro rfl
no goals
α : Type u_1
β : Type ?u.8142
γ : Type ?u.8145
inst✝ : Fintype α
⊢ card univ = Fintype.card α
exact Finset.card_univ