rw [girth_eq_top_iff, indep_iff_forall_subset_not_circuit]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ M.girth = ⊤ ↔ M.Indep M.E
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ (∀ (C : Set α), M.Circuit C → C.Infinite) ↔ ∀ C ⊆ M.E, ¬M.Circuit C