have heI : e ∉ I := by
  intro heI; rw [insert_eq_of_mem heI] at hCI; exact (hC.dep.superset hCI).not_indep hI
α : 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
⊢ 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
⊢ C = M.fundCct e I