exact hJ.subset_cl.trans (M.cl_subset_cl (subset_inter hJ.subset subset_union_right))
case right
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ Y ⊆ M.cl (Y ∩ (I ∪ J))
no goals