exact fun x y ↦ ⟨fun h ↦ ⟨h.eq, h.nonloop_left⟩, by rintro ⟨rfl, h⟩; exact h.parallel_self⟩
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
⊢ ∀ (x y : α), M.Parallel x y ↔ x = y ∧ M.Nonloop x
no goals