rw [hI.conn_eq hJ, (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 : Set α
hI : M.Basis' I X
hJ : M.Basis' J Y
hXY : Disjoint X Y
⊢ M.conn X Y = (M ↾ (I ∪ J))✶.erk
no goals