rw [le_girth_iff]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ 3 ≤ M.girth
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard