simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, dual_base_iff']
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
⊢ ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.Base B ↔ (M✶.map f hf).Base B)
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
⊢ ∀ a ⊆ M.E, ((M.map f hf).Base (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).Base (f '' a)