rwa [sInter_singleton, ← singleton_subset_iff]
case inl.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
x : Set α
hfin : {x}.Finite
hsub : {x} ⊆ Fs
hmod : M.ModularFamily fun x_1 => ↑x_1
hnone : {x}.Nonempty
⊢ ⋂₀ {x} ∈ Fs
no goals