apply conn_eq_encard_of_diff hXY hI hJ (hFI.trans subset_union_left)
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ M.conn X Y = F.encard
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ M.Basis' ((I ∪ J) \ F) (X ∪ Y)