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

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ M.girth < k ↔ ∃ C, M.Circuit C ∧ C.encard < k
Tactic:
simp_rw [girth, iInf_lt_iff, mem_setOf_eq, bex_def]
State after:
no goals