Theorem: Matroid.Basis.mapEmbedding (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α ↪ β
⊢ (M.mapEmbedding f).Basis (⇑f '' I) (⇑f '' X)
Tactic:
apply hIX.map
State after:
no goals