Theorem: Matroid.uniqueBaseOn_rkPos (Matroid/Constructions/Basic.lean)

State before:
α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).Base ∅
Tactic:
simpa [uniqueBaseOn_base_iff hIE] using Ne.symm <| hI.ne_empty
State after:
no goals