rw [← not_nonloop_iff]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.Loop e
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ ¬N.Nonloop e