exact fun f _ hfB hfBi ↦ insert_base_of_insert_indep he hfB hBe hfBi
case refine_2.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)
⊢ ∀ e ∈ M.E, e ∉ B → M.Indep (insert e B) → M.Base (insert e B)
no goals