refine eq_of_indep_iff_indep_forall (by simp [insert_eq_of_mem h.mem_ground_right])
  (fun I hI ↦ ?_)
case mpr.intro
α : 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' = (M' ＼ f).parallelExtend e f
case mpr.intro
α : 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
I : Set α
hI : I ⊆ M'.E
⊢ M'.Indep I ↔ ((M' ＼ f).parallelExtend e f).Indep I