Theorem: Matroid.relRank_mono_left (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ M.relRank X' Y ≤ M.relRank X Y
Tactic:
rw [relRank, relRank, ← union_diff_cancel h, ← contract_contract]
State after:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ (M ／ X ／ (X' \ X)).er Y ≤ (M ／ X).er Y

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X X' Y : Set α
h : X ⊆ X'
⊢ (M ／ X ／ (X' \ X)).er Y ≤ (M ／ X).er Y
Tactic:
apply relRank_le_er
State after:
no goals