rw [loopless_iff_cl_empty] at *
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless
h : (M ／ C).Loopless
⊢ M.Loopless
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).cl ∅ = ∅
h : (M ／ C).cl ∅ = ∅
⊢ M.cl ∅ = ∅