obtain (⟨x, rfl⟩ | X_nt) := hnone.exists_eq_singleton_or_nontrivial
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X 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
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
⊢ ⋂₀ X ∈ Fs
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

case inr
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X 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
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ Fs