rw [base_iff_maximal_indep, ← e.indep_image_iff, and_iff_right hB.indep]
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ N.Base ↑(⇑e '' B)
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ ∀ (I : Set β), N.Indep I → ↑(⇑e '' B) ⊆ I → ↑(⇑e '' B) = I