refine' ⟨fun h B hB ↦ mem_of_mem_of_subset h _, fun h ↦ _⟩
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Loop e ↔ ∀ (B : Set α), M.Base B → e ∈ M.E \ 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

case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
⊢ M.Loop e