convert hI.indep_range_paraMap (fun e ↦ φ e) (by simpa)
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ M.Indep (φ '' I)
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ φ '' I = range fun e => φ ↑e