refine' ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, _⟩,
  fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, _⟩⟩
α : 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}) ↔ ∃ e ∈ C \ I, C = insert e I
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

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
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}