refine' Or.inl ⟨x_dep, fun e_mem ↦ heX (hI.subset (mem_of_mem_insert_of_ne e_mem ne.symm))⟩
case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ (C.extension e).Dep (insert x I) ∧ e ∉ insert x I ∨ x ∈ I
no goals