rw [conn_cl_cl, ← cl_inter_ground, ← cl_inter_ground _ Y, ← conn_cl_cl]
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.conn X Y = M.conn (X ∩ M.E) (Y ∩ M.E)
no goals