Theorem: Matroid.exists_circuit (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 α
inst✝ : M✶.RkPos
⊢ M✶.RkPos
Tactic:
assumption
State after:
no goals