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

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
⊢ M.relRank A A = 0
Tactic:
obtain h := M.relRank_le_encard_diff A A
State after:
α : 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

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