exact (biInter_subset_of_mem hne.some_mem).trans (hne.some.coe_subset_ground)
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ⋂ F ∈ Fs, ↑F ⊆ M.E
no goals