Theorem: Matroid.rk_Pos_iff_exists_cocircuit (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M.RkPos ↔ ∃ K, M.Cocircuit K
Tactic:
rw [← dual_dual M, dual_rkPos_iff_exists_circuit, dual_dual M]
State after:
no goals