Theorem: Matroid.contract_delete_contract' (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D C' : Set α
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D
Tactic:
rw [delete_contract_diff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]
State after:
no goals