exact hC.dep.not_indep <| indep_of_encard_le_two (ENat.le_of_lt_add_one hlt)
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
no goals