simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀