simp [Set.ext_iff, mem_setOf, Nonloop, Loop, mem_diff, and_comm]
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}
no goals