rw [unifOn, truncateTo_base_iff, freeOn_indep_iff, and_iff_right hBE]
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ (unifOn E ↑k).Base B ↔ B.encard = ↑k
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hBE : B ⊆ E
⊢ ↑k ≤ (freeOn E).erk