rw [parallelExtend_nonloop_iff he]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ (M.parallelExtend e f).Nonloop e
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e ∨ e = f