refine' ⟨fun h ↦ _, fun ⟨C, hC, heC, hCX⟩ ↦ _⟩
α : 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
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
case refine'_1
α : 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
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

case refine'_2
α : 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
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ e ∈ M.cl X