exact (h B hB).2 (singleton_subset_iff.mp heB)
case refine'_2.intro.intro
α : 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
he : e ∈ M.E
hei : M.Indep {e}
B : Set α
hB : M.Base B
heB : {e} ⊆ B
⊢ False
no goals