obtain (rfl | hef) := eq_or_ne e f
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
⊢ M.Base (insert f I)
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.Base (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.Base (insert e I)

case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)