rw [he'.parallel_iff_dep hf hef, Dep, pair_subset_iff, and_iff_right he'.mem_ground,
  and_iff_left hf.mem_ground, parallelExtend, restrict_indep_iff, comap_indep_iff,
  image_update, image_id, image_id,
  if_pos (mem_insert_of_mem _ (show f ∈ ({f} : Set α) from rfl))]
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ (M.parallelExtend e f).Parallel e f
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ ¬((M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E)