rwa [Nonloop, and_iff_left (show e ∈ M✶.E from heE), dual_loop_iff_coloop]
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f : α
heE : e ∈ M.E
he : ¬M.Coloop e
hf : f ∉ M.E
⊢ M✶.Nonloop e
no goals