simp only [restrict_ground_eq, image_univ, restrict_indep_iff, image_subset_iff,
  Subtype.coe_preimage_self, subset_univ, and_true]
case h.e'_2.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 (range φ) ↔ (M ↾ range φ).Indep ↑(⇑(isoOfMapParallelRestr ψ ⋯) '' univ)
case h.e'_2.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 (range φ) ↔ M.Indep ((fun a => ↑a) '' range fun a => (isoOfMapParallelRestr ψ ⋯) a)