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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ unifOn E E.encard = freeOn E
Tactic:
rw [unifOn, truncate_eq_self_of_rk_le (freeOn_erk_eq _).le]
State after:
no goals