rwa [← indep_iff_range_indep_of_paraMap (hI.paraMap_injective φ h_para) h_para]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
⊢ M.Indep (range φ)
no goals