rwa [h.eq_of_subset_indep ?_ (subset_diff_singleton hBB' heB), insert_diff_singleton,
  insert_eq_of_mem heB']
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.Base (insert e B)
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
hB : M.Indep B
hBb : ¬M.Base B
B' : Set α
hB' : M.Base B'
hBB' : B ⊆ B'
e : α
heB' : e ∈ B'
heB : e ∉ B
⊢ M.truncate.Indep (B' \ {e})