rw [← restrict_compl, restrict_er_eq', diff_eq, inter_comm M.E, ← inter_assoc, ← diff_eq,
  er_inter_ground_eq]
α : Type u_1
M✝ N : Matroid α
I J C D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
D X : Set α
⊢ (M ＼ D).er X = M.er (X \ D)
no goals