Theorem: Matroid.removeLoops_eq_delete (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 α
⊢ M.removeLoops = M ＼ M.cl ∅
Tactic:
rw [← restrict_compl, removeLoops]
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 α
⊢ M ↾ {e | M.Nonloop e} = M ↾ M.E \ M.cl ∅

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 α
⊢ M ↾ {e | M.Nonloop e} = M ↾ M.E \ M.cl ∅
Tactic:
convert rfl using 2
State after:
case h.e'_3.h.e'_3
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M.E \ M.cl ∅ = {e | M.Nonloop e}

State before:
case h.e'_3.h.e'_3
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M.E \ M.cl ∅ = {e | M.Nonloop e}
Tactic:
simp [Set.ext_iff, mem_setOf, Nonloop, Loop, mem_diff, and_comm]
State after:
no goals