exact disjoint_of_subset_left hfk disjoint_sdiff_left
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
x✝¹ : Disjoint B I
x✝ : B ⊆ M.E
h : M✶.Basis (M.E \ (B ∪ I)) (M.E \ I)
⊢ Disjoint B₀ I
no goals