rw [he.cl, eq_comm] at h'
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {e} = M.cl {f}
⊢ M.Loop f
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {f} = M.cl ∅
⊢ M.Loop f