rw [disjoint_singleton_right, and_iff_left hfJ]
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}
no goals