obtain ⟨I, hI⟩ := M.exists_basis X
α : Type u_1
M✝ : Matroid α
B B' I I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.conn X Y = 0 ↔ M.Skew X Y
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.conn X Y = 0 ↔ M.Skew X Y