rw [← deleteElem, parallelExtend_delete_eq', deleteElem, delete_indep_iff,
  disjoint_singleton_right, and_iff_left hfJ]
case h.e'_2.a
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
J : Set α
hfJ : f ∉ J
⊢ M.Indep J ↔ (M.parallelExtend e f ＼ {f}).Indep J
no goals