rw [← indep_singleton, parallelExtend, restrict_indep_iff, singleton_subset_iff,
  comap_indep_iff, and_iff_left (injOn_singleton _ _), mem_insert_iff,
  image_update, image_id, image_id]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
⊢ (M.parallelExtend e f).Nonloop x ↔ M.Nonloop x ∨ x = f
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
⊢ M.Indep (if f ∈ {x} then insert e ({x} \ {f}) else {x}) ∧ (x = f ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = f