Theorem: Matroid.Basis.to_delete (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 α
h : M.Basis I X
hX : Disjoint X D
⊢ (M ＼ D).Basis I X
Tactic:
rw [delete_basis_iff]
State after:
α : 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

State before:
α : 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
Tactic:
exact ⟨h, hX⟩
State after:
no goals