simp [pair_subset_iff.1 xy_sub]
case x_eq_insert
α : 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 y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})
no goals