Theorem: Matroid.Indep.indep_range_paraMap (Matroid/Parallel.lean)

State before:
α : 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 φ)
Tactic:
rwa [← indep_iff_range_indep_of_paraMap (hI.paraMap_injective φ h_para) h_para]
State after:
no goals