rw [parallelExtend, parallelExtend, deleteElem, delete_ground, insert_diff_singleton,
  eq_iff_indep_iff_indep_forall]
α : 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
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
hef : e ≠ f
⊢ (M.comap (update id f e) ↾ insert f M.E).E = ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).E ∧
    ∀ I ⊆ (M.comap (update id f e) ↾ insert f M.E).E,
      (M.comap (update id f e) ↾ insert f M.E).Indep I ↔ ((M ＼ {f}).comap (update id f e) ↾ insert f M.E).Indep I