exact (h2 e he).1.trans (insert_subset heI Subset.rfl)
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
no goals