rw [biInter_eq_iInter]
α : 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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat ((⋂ i ∈ s, Fs i) ∩ M.E)
α : 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 : α
ι : Type u_2
Fs : ι → Set α
s : Set ι
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat ((⋂ x, Fs ↑x) ∩ M.E)