obtain (rfl | hef) := eq_or_ne 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
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
he' hf : (M.parallelExtend e e).Nonloop e
⊢ (M.parallelExtend e e).Parallel e e

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