rw [delete_basis_iff]
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M.Basis I X
hX : Disjoint X D
⊢ (M ＼ D).Basis I X
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M.Basis I X
hX : Disjoint X D
⊢ M.Basis I X ∧ Disjoint X D