exact fun hxB' ↦ hcl (M.mem_cl_of_mem' ⟨hxB', hx.2⟩ (hH.subset_ground hx.1))
case hxB
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ x ∉ B
no goals