rw [removeLoops_eq_delete, delete_delete, removeLoops_eq_delete, delete_cl_eq, empty_diff,
  union_diff_self, union_eq_self_of_subset_left h]
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : X ⊆ M.cl ∅
⊢ (M ＼ X).removeLoops = M.removeLoops
no goals