rw [Matroid.mapEmbedding, map_base_iff]
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α ↪ β
⊢ (M.mapEmbedding f).Base (⇑f '' B)
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α ↪ β
⊢ ∃ B₀, M.Base B₀ ∧ ⇑f '' B = ⇑f '' B₀