exact ⟨C, hC, heC, heC⟩
case inl.inr.intro.intro
α : 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 : Set α
hC : M.Circuit C
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ e ∈ C
no goals