exact he.not_mem_circuit hK heK
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K✝ : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
K : Set α
hK : M.Circuit K
heK : e ∈ K
⊢ False
no goals