constructor
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f ↔ M'.Parallel e f ∧ M' ＼ f = M
case mp
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M' = M.parallelExtend e f → M'.Parallel e f ∧ M' ＼ f = M

case mpr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ M'.Parallel e f ∧ M' ＼ f = M → M' = M.parallelExtend e f