Theorem: Matroid.delete_compl (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 α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ M ＼ (M.E \ R) = M ↾ R
Tactic:
rw [← restrict_compl, diff_diff_cancel_left hR]
State after:
no goals