rw [← (hHc.diff_singleton_indep he).not_mem_cl_iff_of_not_mem (fun hf' ↦ hf.2 hf'.1),
  hHc.cl_diff_singleton_eq_cl e, hH.flat.cl]
α : 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.Indep (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}))
⊢ f ∉ H