obtain (rfl : e = f) := h_para.eq_of_indep (hI.subset (pair_subset heI hfI))
case pos
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
h_para : M.Parallel' e f
heI : e ∈ I
hfI : f ∈ I
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
case pos
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
hI : M.Indep I
heI : e ∈ I
h_para : M.Parallel' e e
hfI : e ∈ I
⊢ insert e (I \ {e}) = ⇑(Equiv.swap e e) '' I