rintro rfl
α : 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}))
⊢ e ≠ f
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
he : e ∈ I
h_para : M.Parallel' e e
hf : e ∉ I
hI : M.Indep (insert e (I \ {e}))
⊢ False