simp only [simple_iff_forall_pair_indep, map_ground, mem_image, map_indep_iff,
  forall_exists_index, and_imp]
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Simple
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ ∀ ⦃e f_1 : β⦄, ∀ x ∈ M.E, f x = e → ∀ x ∈ M.E, f x = f_1 → ∃ I₀, M.Indep I₀ ∧ {e, f_1} = f '' I₀