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