rw [conn_comm, conn_comm _ X]
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y Y' : Set α
M : Matroid α
X : Set α
hY : Y' ⊆ Y
⊢ M.conn X Y' ≤ M.conn X Y
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y Y' : Set α
M : Matroid α
X : Set α
hY : Y' ⊆ Y
⊢ M.conn Y' X ≤ M.conn Y X