rw [base_iff_maximal_indep, map_indep_iff]
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (M.map f hf).Base B ↔ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ ((∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I) ↔
    ∃ B₀, M.Base B₀ ∧ B = f '' B₀