rw [M.relRank_add_cancel hAB hBX]
α : 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
α : 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