simp only [isoOfSwapParallel_apply_image, Subtype.image_preimage_coe,
  inter_eq_self_of_subset_right hI.subset_ground]
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)
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}) = ⇑(Equiv.swap e f) '' I