exact iff_of_false (fun h ↦ hIE h.subset_ground) (by simp [hIE])
case refine_1.inl
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
no goals