rw [basis'_iff_basis_inter_ground, delete_basis_iff, delete_ground, diff_eq, inter_comm M.E,
  ← inter_assoc, ← diff_eq, ← basis'_iff_basis_inter_ground, and_iff_left_iff_imp,
  inter_comm, ← inter_diff_assoc]
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Basis' I X ↔ M.Basis' I (X \ D)
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M.Basis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D