refine ⟨fun h ↦ ?_, fun ⟨e, he, hBe⟩ ↦ ?_⟩
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.truncate.Base B ↔ ∃ e ∉ B, M.Base (insert e B)
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
h : M.truncate.Base B
⊢ ∃ e ∉ B, M.Base (insert e B)

case refine_2
α : 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.Base B