obtain h := M.relRank_le_encard_diff A A
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
⊢ M.relRank A A = 0
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
h : M.relRank A A ≤ (A \ A).encard
⊢ M.relRank A A = 0