rw [eq_comm, ← dual_delete_dual_eq_contract, ← delete_delete, ← dual_contract_dual_eq_delete, ←
  dual_contract_dual_eq_delete, dual_dual, dual_dual, dual_dual]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K C C₁✝ C₂✝ : Set α
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂)
no goals