simp_rw [← ENat.add_one_le_iff (show 2 ≠ ⊤ by norm_num), show (2 : ℕ∞) + 1 = 3 from rfl,
  simple_iff_three_le_girth, le_girth_iff]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 2 < C.encard
no goals