exact fun hi ↦ hK.dep.not_indep (hi.subset subset_union_left)
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)
no goals