have hwin := e.indep_image_iff (I := M.E ↓∩ I)
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
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
hwin : M.Indep ↑(M.E ↓∩ I) ↔ (unif a b).Indep ↑(⇑e '' M.E ↓∩ I)
⊢ M.Indep I ↔ I.encard ≤ ↑a