refine' Or.inl (dep_iff.2 ⟨fun ind ↦ _, _⟩)
case intro.refine'_2.inr.inl
α : 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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
case intro.refine'_2.inr.inl.refine'_1
α : 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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
⊢ False

case intro.refine'_2.inr.inl.refine'_2
α : 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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ insert x I ⊆ (C.extension e).E