exact ⟨_, (fundCct_subset_insert e I).trans
  (insert_subset he (hI.subset.trans diff_subset)),
  hI.indep.fundCct_circuit ⟨heX, not_mem_subset hI.subset (not_mem_diff_of_mem rfl)⟩⟩
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
I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
no goals