have h_cct := (hB.fundCct_circuit ⟨hxE, hx⟩).mem_cl_diff_singleton_of_mem
  (M.mem_fundCct x B)
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})
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
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ x ∈ M.cl (B \ {e})