by_cases hfI : f ∈ I
case h.e'_3
α : 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
⊢ insert f (I \ {e}) = ⇑(Equiv.swap e f) '' I
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 neg
α : 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