Theorem: Matroid.le_girth_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 : ℕ∞
⊢ k ≤ M.girth ↔ ∀ (C : Set α), M.Circuit C → k ≤ C.encard
Tactic:
simp [girth, le_sInf_iff]
State after:
no goals