exact ⟨by rintro ⟨E, rfl, h⟩; simp [h], fun h ↦ ⟨M.E, by simpa⟩⟩
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
no goals