rwa [indep_iff_range_indep_of_paraMap hφ.injective (by simpa), range_restrict]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep (φ '' I)
hφ : InjOn φ I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ M.Indep I
no goals