Theorem: Matroid.conn_mono_right (Matroid/Connectivity.lean)

State before:
α : 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
Tactic:
rw [conn_comm, conn_comm _ X]
State after:
α : 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

State before:
α : 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
Tactic:
exact M.conn_mono_left hY _
State after:
no goals