rwa [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self heC] at hCI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∉ C
⊢ C ⊆ I
no goals