simp only [ge_iff_le, eq_iff_indep_iff_indep_forall, unifOn_ground_eq, unifOn_indep_iff,
  le_min_iff, and_congr_left_iff, iff_self_and, true_and]
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ unifOn E k = unifOn E (min k E.encard)
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I ⊆ E → I.encard ≤ k → I.encard ≤ E.encard