Theorem: Matroid.delete_basis'_iff (Matroid/Minor/Basic.lean)

State before:
α : 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)
Tactic:
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]
State after:
α : 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

State before:
α : 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
Tactic:
exact fun _ ↦ disjoint_sdiff_left
State after:
no goals