simp [insert_eq_of_mem h.mem_ground_right]
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
hf : f ∉ (M' ＼ f).E
he : M'.Nonloop e ∧ ¬e = f
⊢ M'.E = ((M' ＼ f).parallelExtend e f).E
no goals