rw [← cl_insert_cl_eq_cl_insert, ← hHc.cl_diff_singleton_eq_cl e, cl_insert_cl_eq_cl_insert,
  ← spanning_iff_cl (insert_subset hf.1 (diff_subset.trans hH.subset_ground))] at hcl
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.cl (insert f H) = M.E
⊢ M.Base (insert f (H \ {e}))
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Base (insert f (H \ {e}))