obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans subset_union_left)
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
⊢ M.cl X ⋖[M] M.cl Y
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
⊢ M.cl X ⋖[M] M.cl Y