classical
simp only [parallelExtend, deleteElem, eq_iff_indep_iff_indep_forall, delete_ground,
  restrict_ground_eq, mem_insert_iff, true_or, not_true_eq_false, mem_singleton_iff,
  insert_diff_of_mem, subset_diff, disjoint_singleton_right, delete_indep_iff, restrict_indep_iff,
  comap_indep_iff, ne_eq, image_update, id_eq, image_id', mem_diff, update_id_injOn_iff,
  and_congr_left_iff, and_imp, true_and]
rintro I - hf -
simp only [hf, not_false_eq_true, diff_singleton_eq_self, ite_false, IsEmpty.forall_iff, and_true,
  and_iff_left_iff_imp]
exact fun hI ↦ hI.subset_ground.trans <| subset_insert _ _
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ M.parallelExtend e f ＼ f = M ＼ f
no goals