have hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f}) := by
  rw [← M.parallelExtend_delete_eq e hf, deleteElem, delete_cl_eq, mem_diff,
    (parallelExtend_parallel he f).mem_cl_iff_mem_cl] at heX
  simpa [(show e ≠ f by rintro rfl; exact hf he.mem_ground)] using heX
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : e ∉ M.cl X
hfX : f ∉ X
hfX' : f ∉ (M.parallelExtend e f).cl (X \ {f})
⊢ (M.parallelExtend e f).cl X = (M.parallelExtend e f ＼ f).cl X