rw [hI.conn_eq hJ, hF'.erk_dual_restrict, diff_diff_cancel_left hFIJ,
  (hXY.mono hI.subset hJ.subset).inter_eq, encard_empty, zero_add]
α : 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
hFIJ : F ⊆ I ∪ J
hF : M.Basis' ((I ∪ J) \ F) (X ∪ Y)
hF' : M.Basis ((I ∪ J) \ F) (I ∪ J)
⊢ M.conn X Y = F.encard
no goals