obtain ⟨e, he⟩ := exists_of_ssubset
  (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
h : M.Basis I C
⊢ ∃ e ∈ C, I = C \ {e}
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
h : M.Basis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}