Theorem: Matroid.unif_er_eq (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X✝ C : Set α
k : ℕ∞
a b a' b' : ℕ
X : Set (Fin b)
⊢ (unif a b).er X = min X.encard ↑a
Tactic:
rw [unif, unifOn_er_eq _ _ (subset_univ _)]
State after:
no goals