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]
α : 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
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ ∀ I ⊆ M.E,
    f ∉ I →
      f ∉ I →
        ((M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I)