rw [diff_subset_iff, contract_loops_eq, union_diff_self,
  union_eq_self_of_subset_left (M.subset_cl I)]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X \ I ⊆ (M ／ I).cl ∅
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X ⊆ M.cl I