rw [truncate_indep_iff]
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.truncate.Indep B
case refine_2.refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : ∃ e ∉ B, M.Base (insert e B)
e : α
he : e ∉ B
hBe : M.Base (insert e B)
⊢ M.Indep B ∧ ¬M.Base B