refine' fun x ↦ ⟨fun x_mem ↦ _, fun (x_mem) ↦ _⟩
case intro
α : 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 ∈ (C.extension e).cl I ↔ x ∈ insert e (M.cl I)
case intro.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 ∈ (C.extension e).cl I
⊢ x ∈ insert e (M.cl I)

case intro.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 ∈ insert e (M.cl I)
⊢ x ∈ (C.extension e).cl I