rw [hI.conn_eq hJ, hI.basis_cl_right.basis'.conn_eq hJ]
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.conn X Y = M.conn (M.cl X) Y
no goals