obtain ⟨I, hI⟩ := M.exists_basis (X \ {e}) (diff_subset.trans hXE)
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
case intro.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})
I : Set α
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C