refine ⟨fun ⟨⟨⟨e,he⟩, hCI, hCE⟩, h2⟩ ↦ ⟨e, ⟨hCE he, fun heI ↦ hCI ?_⟩, ?_⟩, ?_⟩
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ ((C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E) ↔ ∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}
case refine_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
heI : e ∈ I
⊢ C ⊆ I

case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C = {e}

case refine_3
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}) → (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E