simp_rw [girth, le_iInf_iff, one_le_encard_iff_nonempty]
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ 1 ≤ M.girth
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ ∀ i ∈ {C | M.Circuit C}, i.Nonempty