simpa only [sdiff_self, Set.bot_eq_empty, Set.encard_empty, nonpos_iff_eq_zero] using h
α : 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
no goals