simpa [diff_singleton_eq_self he, hfI]
  using heI.exchange_base_of_indep (e := e) (f := f) (by simp [hef.symm, hf])
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)
no goals