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

State before:
α : Type u_1
E I : Set α
hE : E.Nonempty
⊢ (freeOn E).RkPos
Tactic:
rw [← uniqueBaseOn_self]
State after:
α : Type u_1
E I : Set α
hE : E.Nonempty
⊢ (uniqueBaseOn E E).RkPos

State before:
α : Type u_1
E I : Set α
hE : E.Nonempty
⊢ (uniqueBaseOn E E).RkPos
Tactic:
exact uniqueBaseOn_rkPos Subset.rfl hE
State after:
no goals