simp_rw [← image_univ, image_image, image_univ]
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep ((fun a => ↑a) '' range fun a => (isoOfMapParallelRestr ψ ⋯) a)
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep (range fun x => ↑((isoOfMapParallelRestr ψ ⋯) x))