rw [subset_diff, and_iff_right (cl_subset_ground _ _), disjoint_iff_inter_eq_empty,
  hB.indep.cl_inter_eq_self_of_subset (empty_subset B)]
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : M.Loop e
B : Set α
hB : M.Base B
⊢ M.cl ∅ ⊆ M.E \ B
no goals