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

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M : Matroid α
h : M.Circuit ∅
⊢ False
Tactic:
simpa using h.nonempty
State after:
no goals