obtain (hxI' | hxI') := em (f x ∈ f '' I)
case intro.intro.intro.h.inr.inr
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)
case intro.intro.intro.h.inr.inr.inl
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
hxI' : f x ∈ f '' I
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)

case intro.intro.intro.h.inr.inr.inr
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
hss : insert x I ⊆ (M.comap f).E
hxI' : f x ∉ f '' I
⊢ M.Indep (f '' insert x I) → f x ∈ f '' I ↔ x ∈ f ⁻¹' M.cl (f '' X)