Theorem: Matroid.delete_cl_eq (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 X : Set α
⊢ (M ＼ D).cl X = M.cl (X \ D) \ D
Tactic:
rw [← restrict_compl, restrict_cl_eq', sdiff_sdiff_self, bot_eq_empty, union_empty,
  diff_eq, inter_comm M.E, ← inter_assoc X, ← diff_eq, cl_inter_ground,
  ← inter_assoc, ← diff_eq, inter_eq_left]
State after:
α : 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 X : Set α
⊢ M.cl (X \ D) \ D ⊆ M.E

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 X : Set α
⊢ M.cl (X \ D) \ D ⊆ M.E
Tactic:
exact diff_subset.trans (M.cl_subset_ground _)
State after:
no goals