exact False.elim <| he'.not_connected hM h
case inl.inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
he' : M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
no goals