exact fun h ↦ (hB.indep.nonloop_of_mem heB).not_loop <| h (hB.subset_ground heB)
case intro.intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e✝ f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
e : α
heB : e ∈ B
⊢ ¬M.E ⊆ M.cl ∅
no goals