exact Flat.iInter (fun ⟨F, hF⟩ ↦ h _ hF)
α : 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 (Set α)
hF : Fs.Nonempty
h : ∀ F ∈ Fs, M.Flat F
this : Nonempty ↑Fs
⊢ M.Flat (⋂ i, ↑i)
no goals