simpa [inter_insert_eq hne] using subset_inter (h2 f hf).1 (h2 f' hf').1
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
f : α
hf : f ∈ C
f' : α
hf' : f' ∈ C
hne : ¬f = f'
⊢ C ⊆ I
no goals