simp_rw [← hf.image_diff_subset hB, map_image_base_iff diff_subset,
  map_image_base_iff (show B ⊆ M✶.E from hB), dual_base_iff hB, and_iff_left_iff_imp]
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).Base (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).Base (f '' B)
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ M.Base (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B