have hiX : ⋂₀ Js ⊆ I := (sInter_subset_of_mem hne.some_mem).trans (hIs _ hne.some_mem)
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)