use fun h ↦ h.coloops_subset.antisymm' (by rwa [sdiff_eq_left.mpr h.indep.disjoint_loops] at hBE)
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base B ↔ B = M✶.cl ∅
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ B = M✶.cl ∅ → M.Base B