rintro ⟨I, X, hIX, rfl, rfl⟩
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).Basis I X
case refine_2.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 X : Set α
hIX : M.Basis I X
⊢ (M.map f hf).Basis (f '' I) (f '' X)