obtain rfl : I = BX ∩ X := hI.eq_of_subset_indep (hBXb.indep.inter_right _)
  (subset_inter hIBX hI.subset) inter_subset_right
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBX : M.Basis BX (I ∪ J)
hIBX : I ⊆ BX
hIJE : M.Spanning (I ∪ J)
hBXb : M.Base BX
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
case intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)