obtain ⟨⟨e, he, heX⟩, hXE⟩ := hX
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (∃ e ∈ X, e ∈ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C