refine fun x hx ↦ by_contra fun hcl ↦ ?_
case 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
⊢ H \ {e} ⊆ M.cl (B \ {e})
case 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
x : α
hx : x ∈ H \ {e}
hcl : x ∉ M.cl (B \ {e})
⊢ False