rw [map_basis_iff _ _ hI hX] at h
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) ((fun a => f a) '' X)
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀