refine ⟨fun x hx ↦ ⟨f.apply_mem hx, ⟨x, hx, rfl⟩⟩, ?_⟩
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ (∀ (a : α), M.Nonloop a → M.Nonloop (f a) ∧ ∃ x, M.Nonloop x ∧ f x = f a) ∧
    ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ∀ (e f_1 : α), M.Parallel e f_1 → ∀ (x : α), M.Nonloop x → f x = e → ∀ (x : α), M.Nonloop x → f x = f_1 → e = f_1