refine ⟨fun _ _ ↦ Circuit.finite, fun h ↦
  ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩ ⟩
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Finitary ↔ ∀ (C : Set α), M.Circuit C → C.Finite
case refine_1
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

case refine_2
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E