refine (h _ ⟨hfH, fun hfB ↦ hfBe ⟨hfB, fun (hfe : f = e) ↦ ?_⟩⟩).2 hfB.symm
case intro.intro.intro
α : 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})
hb : M.Basis (B \ {e}) H
f : α
hfB : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
⊢ False
case intro.intro.intro
α : 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})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ False