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

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
hX : X ⊆ E
⊢ (unifOn E k).er X = min X.encard k
Tactic:
rw [unifOn, truncateTo_er_eq, freeOn_er_eq hX]
State after:
no goals