obtain (⟨x, rfl⟩ | X_nt) := X_none.exists_eq_singleton_or_nontrivial
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
⊢ ⋂₀ X ∈ C
case inl.intro
α : Type u_1
α✝ : Type u_2
C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
x : Set α✝
X_fin : {x}.Finite
X_sub : {x} ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : {x}.Nonempty
⊢ ⋂₀ {x} ∈ C

case inr
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ C