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

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