refine ⟨C', hC', ?_, hC'CI.trans (union_subset_union_right _ hI.subset)⟩
case intro.intro.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
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
case intro.intro.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
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
⊢ C ⊆ C'