nth_rw 2 [← M.parallelExtend_delete_eq e hf]
α : 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
⊢ (M.parallelExtend e f).cl X = insert f (M.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
⊢ (M.parallelExtend e f).cl X = insert f ((M.parallelExtend e f ＼ f).cl X)