simpa using fundCct_subset_insert _ _
case intro.inr.refine_1
α : 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})
⊢ M.fundCct x B \ {x} ⊆ B
no goals