simp [Subset.rfl]
case h.e'_1.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 I ↔ (M ↾ I).Indep ↑univ
no goals