Theorem: RankMatroid.relRank_mono_left (Matroid/Constructions/RankAxioms.lean)

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hBX : B ⊆ X
hAB : A ⊆ B
⊢ M.relRank B X ≤ M.relRank A X
Tactic:
rw [M.relRank_add_cancel hAB hBX]
State after:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hBX : B ⊆ X
hAB : A ⊆ B
⊢ M.relRank B X ≤ M.relRank A B + M.relRank B X

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hBX : B ⊆ X
hAB : A ⊆ B
⊢ M.relRank B X ≤ M.relRank A B + M.relRank B X
Tactic:
simp only [self_le_add_left]
State after:
no goals