rw [← not_indep_iff]
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ M.Dep (C ∪ I)
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ ¬M.Indep (C ∪ I)