obtain (hIE | hIE) := em' <| I ⊆ M.E
case refine_1
α : 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 α
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
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

case refine_1.inr
α : 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