rw [unif, unifOn, truncateTo_base_iff, freeOn_indep_iff, and_iff_right (subset_univ _)]
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ (unif a b).Base B ↔ B.encard = ↑a
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ ↑a ≤ (freeOn univ).erk