suffices hsub : C.Subsingleton from hsub.eq_singleton_of_mem he
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_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.Subsingleton