Theorem: Matroid.delete_contract_diff (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 α
D C : Set α
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
Tactic:
rw [contract_eq_contract_iff, delete_ground, diff_inter_diff_right, diff_eq, diff_eq, inter_assoc]
State after:
no goals