simp only [deleteElem, delete_nonloop_iff, mem_singleton_iff] at he
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
he : (M' ＼ f).Nonloop e
hf : f ∉ (M' ＼ f).E
⊢ M' = (M' ＼ f).parallelExtend e f
case mpr.intro
α : 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
⊢ M' = (M' ＼ f).parallelExtend e f