Theorem: encard_univ_fin (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n a : ℕ
⊢ univ.encard = ↑a
Tactic:
simp [encard_eq_coe_toFinset_card]
State after:
no goals