have hf : (M.parallelExtend e f).Nonloop f := by
  rw [parallelExtend_nonloop_iff he]; right; rfl
α : 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
⊢ (M.parallelExtend e f).Parallel e f
α : 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
⊢ (M.parallelExtend e f).Parallel e f