obtain ⟨hCE, hCI⟩ := hCss
case intro
α : 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
hCss : C ⊆ M.E ∧ Disjoint C I
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
case intro.intro
α : 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
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K