refine ⟨fun h C hC ↦ le_of_not_lt fun hlt ↦ ?_, fun h ↦ ?_⟩
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
C : Set α
hC : M.Circuit C
hlt : C.encard < 3
⊢ False

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ M.Simple