simp [insert_diff_singleton_comm hef, insert_eq_of_mem he, diff_singleton_eq_self hf]
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h_para : M.Parallel' e f
he : e ∈ I
hf : f ∉ I
hI : M.Indep (insert f (I \ {e}))
hef : e ≠ f
⊢ I = insert e (insert f (I \ {e}) \ {f})
no goals