rintro ⟨h, rfl⟩
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
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
M' : Matroid α
e f x : α
I C : Set α
h : M'.Parallel e f
he : (M' ＼ f).Nonloop e
hf : f ∉ (M' ＼ f).E
⊢ M' = (M' ＼ f).parallelExtend e f