suffices M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I by
  simpa [hfI, parallelExtend, Ne.symm he.2, hI.trans (subset_insert _ _)]
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I
case mpr.intro.inr
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I✝ C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
I : Set α
hI : I ⊆ M'.E
hfI : f ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I