simpa
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
x✝ : M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
hE : M.E = E
h : ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
⊢ M.E = (unifOn E k).E
no goals