nth_rw 2 [← 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}) 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.Basis (C \ {e}) (insert e C)