convert (isoOfSwapParallel h_para).image_indep (I := M.E ↓∩ I)
  (by rwa [Subset.image_val_preimage_val_eq hI.subset_ground])
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ M.Indep (insert f (I \ {e}))
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
⊢ insert f (I \ {e}) = ↑(⇑(isoOfSwapParallel h_para) '' M.E ↓∩ I)