rintro ⟨e, he, rfl⟩
case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) → M.Basis I C
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
C C' X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ M.Basis (C \ {e}) C