rw [← loop_iff_mem_cl_empty, ← singleton_dep, hI.indep.contract_dep_iff,
  disjoint_singleton_left, and_iff_right he.2, singleton_union,
  ← hI.indep.mem_cl_iff_of_not_mem he.2]
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ (M ／ I).cl ∅
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ M.cl I