Theorem: Matroid.contract_eq_delete_of_subset_loops (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hX : X ⊆ M.cl ∅
⊢ M ／ X = M ＼ X
Tactic:
rw [← dual_inj, contract_dual_eq_dual_delete, delete_dual_eq_dual_contract, eq_comm,
  contract_eq_delete_of_subset_coloops]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hX : X ⊆ M.cl ∅
⊢ X ⊆ M✶✶.cl ∅

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hX : X ⊆ M.cl ∅
⊢ X ⊆ M✶✶.cl ∅
Tactic:
rwa [dual_dual]
State after:
no goals