refine' ⟨⟨mem_insert _ _, he⟩, hI.indep, hX⟩
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∉ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ insert x I \ M.E ∧ M.Indep I ∧ M.cl X ∉ C
no goals