obtain (hx | hx) := em (x ∈ B)
case intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (B \ {e})
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∈ B
⊢ x ∈ M.cl (B \ {e})

case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.cl (B \ {e})