simp [heI, heC]
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
no goals