Theorem: Matroid.delete_comm (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 : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁
Tactic:
rw [delete_delete, union_comm, delete_delete]
State after:
no goals