exact fun _ h _ ↦ (image_subset_iff.1 h.indep.subset_ground)
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ InjOn f I → N.Basis (f '' I) (f '' X ∩ N.E) → I ⊆ X → I ⊆ f ⁻¹' N.E
no goals