rwa [← (hB.indep.diff {e}).not_mem_cl_iff_of_not_mem (not_mem_subset diff_subset hxB)
  (hH.subset_ground hx.1)]
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})
hxB : x ∉ B
⊢ M.Indep (insert x (B \ {e}))
no goals