rintro ⟨e, ⟨heI,heC⟩, rfl⟩
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
case refine_3.intro.intro.intro
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
e : α
heI : e ∈ E
heC : e ∉ I
⊢ ({e}.Nonempty ∧ ¬{e} ⊆ I ∧ {e} ⊆ E) ∧ ∀ e_1 ∈ {e}, {e} ⊆ insert e_1 I ∧ {e} ⊆ insert e_1 E