simp only [parallelExtend, deleteElem, eq_iff_indep_iff_indep_forall, restrict_ground_eq,
  addLoop_ground, delete_ground, mem_diff, mem_singleton_iff, not_true_eq_false, and_false,
  insert_diff_singleton, restrict_indep_iff, comap_indep_iff, ne_eq, image_update, id_eq,
  image_id', update_id_injOn_iff, addLoop_indep_iff, delete_indep_iff, disjoint_singleton_right,
  true_and]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : ¬M.Nonloop e
f : α
⊢ M.parallelExtend e f = (M ＼ f).addLoop f
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : ¬M.Nonloop e
f : α
⊢ ∀ I ⊆ insert f M.E,
    (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 ∧ f ∉ I