simp [heI, show ¬ M'.Indep I from
  fun hI ↦ he.2 (h.eq_of_indep (hI.subset (pair_subset heI hfI)))]
case mpr.intro.inr.inl
α : 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
heI : e ∈ I
⊢ M'.Indep I ↔ M'.Indep (insert e (I \ {f})) ∧ e ∉ I
no goals