Pullback and pseudoelements Let $\mathcal{A}$ be an abelian category, and let $X$ an object of $\mathcal{A}$. Recall that a pseudoelement of $X$ is an equivalence class of arrows $X_1 \to X$, where $x_1 \colon X_1 \to X$ and $x_2 \colon X_2 \to X$ are equivalent if there is an object $P$ and epimorphisms $p_1 \colon P \to X_1$ and $p_2 \colon P \to X_2$ such that $x_1 \circ p_1= x_2 \circ p_2$.  We write $x \in^\ast X$ to denote that $x$ is a pseudoelement of $X$. If $x \in^\ast X$ and $f \colon X \to Y$, then $f(x) \in^\ast Y$ is obtained by composition.
Pseudoelements are pretty nice, for example a morphism is equal to $0$ if and only if it sends all pseudoelements to $0$, and we can characterize monomorphisms (resp. epimorphisms) in terms of pseudoelements, as one expects. Similarly we can check if a sequence is exact by testing exactness on pseudoelements. Of course there are limitations, for example we can not test if two morphisms are equal on pseudoelements (in contrast with the Freyd–Mitchell embedding theorem).
A natural problem is what happens with pullbacks. Let $f \colon X \to Z$ and $g \colon Y \to Z$ be morphisms, and let $x \in^\ast X$ and $y \in^\ast Y$ such that $f(x) = g(y)$. It's easy to construct $s \in^\ast X \times_Z Y$ such that $\pi_1(s) = x$ and $\pi_2(s) = y$, by universal property of the pullback. Now, we would like $s$ to be unique, and indeed Francis Borceux in his "Handbook of Categorical Algebra: Volume 2", Proposition 1.9.5, claims so. The proof is only sketched, and essentially Borceux says "All the relevant epimorphisms can, by successive pullbacks, be replaced by epimorphisms with the same domain, from which the claim follows". It's not completely clear how to write down the details, see for example this stackexchange question, with a partial answer.
I've tried to prove the theorem by myself, essentially following Borceux's idea of constructing several pullbacks, but I am unable to finish the proof. To simplify the notation, let's consider the case of the product, so $Z=0$ in the above discussion. Let $a \colon A \to X \times Y \in^\ast X \times Y$ and $b \colon B \to X \times Y \in^\ast X \times Y$ be such that $\pi_1(a)=\pi_1(b)$ and $\pi_2(a)=\pi_2(b)$. So there are epimorphisms $a_1 \colon Z_1 \to A$, $b_1 \colon Z_1 \to B$, $a_2 \colon Z_2 \to A$ and $b_2 \colon Z_2 \to B$ such that $\pi_1 \circ a \circ a_1 = \pi_1 \circ b \circ b_1$ and $\pi_2 \circ a \circ a_2 = \pi_2 \circ b \circ b_2$. To construct the required epimorphisms we consider $P_a = Z_1 \times_A Z_2$ and $P_b = Z_1 \times_B Z_2$. We finally set $P = P_a \times_{Z_1} P_b$, where $P_a \to Z_1$ and $P_b \to Z_1$ are the first projections. We write $f_a : P \to A := a_1 \circ \pi_1 \circ \pi_1$ (two different $\pi_1$) and $f_b : P \to B := b_1 \circ \pi_1 \circ \pi_2$. Then $f_a$ and $f_b$ are epimorphisms. We need to prove that $a \circ f_a= b \circ f_b$ and it is enough to prove that $\pi_1 \circ a \circ f_a= \pi_1 \circ b \circ f_b$ and $\pi_2 \circ a \circ f_a= \pi_2 \circ b \circ f_b$. The first one follows immediately by $\pi_1 \circ a \circ a_1 = \pi_1 \circ b \circ b_1$ and the commuting square of the pullback. I don't see how to prove the second equality, I tried essentially all the combinations of the two equalities we have and all the pullback squares, but it didn't work.
Of course one can try to construct different epimorphisms, but all the constructions I tried (even those more symmetric then the one above) end up with exactly the same equality to prove.
Does someone know a complete proof of this result? Thanks!
PS: I realized I am not able to prove it trying to formalize the result in Lean, in a lemma for the Liquid Tensor Experiment, you can see the actual Lean code here.
 A: The claim stated in the question is false, and the statement of Lemma 1.9.5 in Borceux is unclear, but seems wrong.  To be clear, the claim in this question is that for any Abelian category $\newcommand{\A}{\mathcal{A}}\A$, and maps $f:X \to Z$, $g : Y \to Z$, and pseudo-elements $[x]$, $[y]$ such that $f[x] = g[y]$, there is a $unique$ pseudo-element $[p]$ of $X \times_Z Y$ with $\pi_1[p] = [x]$, $\pi_2[p]=[y]$. More concisely, the claim is that the “pseudo-elements” functor $\A \to \mathrm{Set}$ preserves pullbacks.  (Borceux Lemma 1.9.5 claims that $[p]$ is “pseudo-unique”; from the “proof” sketch, I agree it seems like he intends this to mean “unique, as a pseudo-element”, but conceivably he had something else in mind.)
Work for concreteness in $\newcommand{\Ab}{\mathrm{Ab}}\Ab$.  Then maps $x_1 \colon X_1 \to X$, $x_2 \colon X_2 \to X$ are equivalent as pseudo-elements if and only if they have the same image.  (The “only if” direction is clear; for the “if”, note that in this case the projections $X_1 \times_X X_2 \to X_i$ are epi.)  So pseudo-elements of $X$ correspond to subobjects/subgroups of $X$.  Borceux notes this fact in the closing discussion of §1.9.
But now it’s easy to see this doesn’t preserve pullbacks. For instance, it doesn’t preserve the product $\newcommand{\Q}{\mathbb{Q}} \Q \times \Q$: the subgroups $\{ (x,x) | x \in \Q \}$ and $\{ (x,2x) | x \in \Q \}$ have the same images under each projection, but are not the same.  In terms of pseudo-elements, the maps $s_1, s_2 : \Q \to \Q \times \Q$ given by $s_i(x)=(x,ix)$ are not equal as pseudo-elements of $\Q \times \Q$, but their images under each projection are equal as pseudo-elements of $\Q$.
A: Claim:
Consider a category, such that for any two objects $X,Y$ there exists an object $Z$ and  epimorphisms $Z\twoheadrightarrow X$ and $Z\twoheadrightarrow Y$.
We call such a $Z$ and the epis a common cover of $X$ and $Y$.
Let

be a Cartesian square.
We shall write $[p]$ for a generalized element with representative $p$.
Let $[p],[p']$ be two generalised elements of $P$ such that $f^*([p])=f^*([p'])$ and $g^*([p])=g^*([p'])$.
Then $[p]=[p']$.
Proof:
Replacing the domains of $p$ and $p'$ with a common cover, we can assume, that they have the same domain $D$.
The equation $g^*(p)=g^*(p')$ means that we have two commutative  diagrams

withe the same $eta$.
We can replace $D$ by $D'$ and get a diagram

which commutes for $p$ and for $p'$ separately.
In the same way we get an arrow $D\to B$ such that the diagram

which commutes for $p$ and for $p'$.
But now the uniqueness in the definition of a Cartesian square yields $p=p'$.
