classical
rw [parallelExtend, parallelExtend, deleteElem, delete_ground, insert_diff_singleton,
  eq_iff_indep_iff_indep_forall]
simp only [restrict_ground_eq, restrict_indep_iff, comap_indep_iff, ne_eq, image_update, id_eq,
  image_id', mem_diff, mem_singleton_iff, update_id_injOn_iff, delete_indep_iff,
  disjoint_singleton_right, and_congr_left_iff, iff_self_and, true_and]
aesop
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ M.parallelExtend e f = (M ＼ f).parallelExtend e f
no goals