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

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ (unifOn E k).erk = min E.encard k
Tactic:
rw [erk_eq_er_ground, unifOn_ground_eq, unifOn_er_eq _ _ Subset.rfl]
State after:
no goals