obtain (he' | he') := em (M.Coloop e)
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.Connected
hM : M.E.Nontrivial
he hf : e ∈ M.E
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
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

case inl.inr
α : 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