exact hC.dep.not_indep <| hI _ hCI (h C hC)
case refine_1.intro.intro
α : 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
C : Set α
hCI : C ⊆ I
hC : M.Circuit C
⊢ False
no goals