Theorem: Matroid.simple_iff_forall_circuit (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 2 < C.encard
Tactic:
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]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ 2 ≠ ⊤
Tactic:
norm_num
State after:
no goals