rw [← insert_diff_singleton, (hC.diff_singleton_indep he).basis_insert_iff,
  insert_diff_singleton, insert_eq_of_mem he]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Basis (C \ {e}) (insert e C)
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}