rw [diff_singleton_eq_self (by simp [Ne.symm hxe, heI.2]), hI.insert_indep_iff_of_not_mem hxI,
  hI'.flat.cl]
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ M.Indep (insert x I \ {e})
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ x ∈ M.E \ I