rintro rfl
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E k → M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).E = E ∧ ∀ (I : Set α), (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E