obtain hBH := hH.eq_of_subset (hB.hyperplane_of_cl_diff_singleton he) h1
α : 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
h1 : H ⊆ M.cl (B \ {e})
⊢ False
α : 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
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ False