rw [← inter_union_diff (s := M.cl ∅) (t := C), hC.1, empty_union, diff_eq_empty]
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ = ∅
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : M.cl ∅ ∩ C = ∅ ∧ C \ M.E = ∅
h : M.cl C ⊆ C
⊢ M.cl ∅ ⊆ C