convert (delete_indep_iff (M := M.parallelExtend e f) (D := {f}) (I := J)).symm using 1
α : 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.parallelExtend e f).Indep J ↔ M.Indep J
case h.e'_1.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.parallelExtend e f).Indep J ↔ (M.parallelExtend e f).Indep J ∧ Disjoint J {f}

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