rw [← hI.cl_eq_cl] at h
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
I : Set α
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
I : Set α
h : e ∈ M.cl I
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X