rw [← restrict_compl, removeLoops]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M.removeLoops = M ＼ M.cl ∅
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M ↾ {e | M.Nonloop e} = M ↾ M.E \ M.cl ∅