have he : e ∈ M.cl I := by
  rw [mem_cl_iff_exists_circuit_of_not_mem heI]; exact ⟨C, hC, heC, hCI⟩
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ C = M.fundCct e I
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
⊢ C = M.fundCct e I