simp only [truncate_ground_eq, mem_diff, truncate_indep_iff, not_and, not_not, and_imp]
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.truncate.E \ B, ¬M.truncate.Indep (insert e B)
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)