When I originally asked this question (see below), I was looking for any solution, but I was not completely satisfied with Saving's answer as some of the details were unclear to me. So I came up with my own partial solution (we indeed tend to understand our own solutions better), but just one step in my proof is lacking. I am now seeking the completion of my own proof or a proof of the overall goal (showing that a finite set is countable in ETCS) but which is very clear and uses the axioms of ETCS as sat out by Lawvere. Ideally someone could just complete my proof.
My partial proof:
First some definitions:
$$\mathrm{OR} : \Omega \times \Omega \to \Omega$$ $$\mathrm{EQ} = \chi_{\delta_X} : X \times X \to \Omega$$ $$\mathrm{distribute\_left} : X \times (Y \times Z) \to (X \times Y) \times (X \times Z)$$
$\Omega = \{\mathsf{t},\mathsf{f}\}$ and $\mathrm{OR}\circ \langle p,q\rangle = \mathsf{t}$ just in case at least one of $p$ or $q$ is $\mathsf{t}$, and $\mathrm{OR}\circ \langle \mathsf{f}, \mathsf{f}\rangle = \mathsf{f}$. $\mathrm{EQ}$ is the equality predicate, it evaluates to true if both elements of the pair are equal; otherwise it evaluates to false. And $\mathrm{distribute\_left}$ is a defined by $\mathrm{distribute\_left} \langle x, \langle y, z\rangle\rangle = \langle\langle x, y\rangle, \langle x, z\rangle\rangle$.
TO SHOW: $u : \mathbb{N} \to (\Omega^X \times X) \coprod 1$ is an epimorphism.
Afterward, the rest easily follows: pick an arbitrary element $x : 1 \to X$ (exists since $X$ is finite, or apply the axiom of choice to $\beta_X$), and obtain $(\pi_1 \amalg x) \circ u : \mathbb{N} \to X$.
$(\pi_1 \amalg x) : (\Omega^X \times X) \coprod 1 \to X$ should also be an epimorphism (any element of $X$ can be output by providing it as part of the input, regardless of the $\Omega^X$), so $(\pi_1 \amalg x) \circ u$ is also an epimorphism, making $X$ countable.
ORIGINAL POST:
In ETCS a set $X$ is finite if for any map injective map $m: X \to X$ it is the case that $m$ is a bijection. A set $Y$ is countable if there exists an epimorphism $e: \mathbb{N}\to Y$. Side note: I personally don't like this definition, since it seems that the emptyset is then not countable. I believe that a better definition for countable is: $Y$ is countable if there exists an injective map $j : Y \to \mathbb{N}$. It seems these definitions are nearly equivalent by the AC.
In any case, I would like to prove that every finite set is countable, and I would especially appreciate a hint rather than a full solution. Thank you
Edit: after learning more about ETCS, I have come up with a much more concise proof which fully leverages the power of well-pointedness.
We first do a brief review of the properties of ETCS.
We write $x :\in X$ as shorthand for $x : 1 \to X$. Given an element $x :\in X$ and a function $f : X \to Y$, we write $f(x)$ as a shorthand for the element $f \circ x :\in Y$. If we have a monic $i_S : S \to X$, we write for shorthand $S \subseteq X$. Given an element $x :\in X$ and a subset $S \subseteq X$, we write $x \in S$ for the proposition $\exists y \in S (i_S(y) = x)$ (that is, that $x$ factors through the monic $i_S$).
Note that a map $f : X \to Y$ is mono iff for all $a, b :\in X$, if $f(a) = f(b)$ then $a = b$. This follows from the fact that $1$ is a generator and that all monos are regular. This can be summarized by saying monos are exactly injections on elements.
Note further that a map $f : X \to Y$ is epi iff for all $y \in Y$, there exists $x \in X$ such that $f(x) = y$. This follows from considering that $f$ is an epi iff the image of $f$ (call it $K$) equals $Y$ iff for all $y \in Y$, $y \in K$. But we see that if $y \in K$, then let $f' : X \to K$ be the epi image map: then $y^*(f)$ is an epi into 1, which has a section, which provides some $x \in X$ such that $f'(x) = y$. This can be summarized by saying that epis are exactly surjections on elements.
From these facts, it follows that $f : X \to Y$ is an isomorphism iff for all $y \in Y$ there is a unique $x \in X$ such that $f(x) = y$, since an isomorphism is a mono-epi. This can be summarized by saying that isomorphisms are exactly bijections on elements.
Define a $\Delta_0$ logical statement to be one formed with atomic propositions of the form $a = b$ where $a, b : X \to Y$, and where all quantifiers are $\Delta_0$ quantifiers (that is, of the form $\forall x :\in X$ or $\exists x :\in X$).
Now further recall the principle of $\Delta_0$ separation, which states that for any $\Delta_0$ logical statement $\phi(x)$ with the variable typing $x :\in X$, there exists a (necessarily unique) subobject $S \in X$ such that for all $x :\in X$, $x \in S$ iff $\phi(x)$. A statement where all quantifiers are $\Delta_0$ is called a $\Delta_0$-statement. Note that because arrows $X \to Y$ are in natural bijection with elements $1 \to Y^X$, we can extend $\Delta_0$-separation to include quantifiers over any arrow variables since such a statement is logically equivalent to one with quantifications over elements $:\in Y^X$. We will write the subobject defined this way as $\{x :\in X | \phi(x)\}$.
The proof of $\Delta_0$ separation is a simple induction on formulas (simple if you understand the structure of a topos, that is). The Heyting Algebra structure of subobjects handles the case of $\top, \bot, \implies, \land, \lor,$ and $\neg$. Equalisers handle the atomic propositions $f = g$. And existential and universial quantifiers are handled using the left and right adjoints to pullback.
Similarly, we can also quantify over subobjects since subobjects of $X$ correspond up to isomorphism with arrows $1 \to P(X)$ and the truth of a $\Delta_0$ statement is preserved under isomorphisms. However, we will not require this fact.
From this principle, we have the principle of $\Delta_0$ function definition. Let $\phi(x, y)$ be a $\Delta_0$ statement with variable typing $x :\in X$, $y :\in Y$ such that $\forall x :\in X \exists! y :\in y \phi(x, y)$. Then there is a unique function $f : X \to Y$ such that $\forall x :\in X, \phi(x, f(x))$. This follows by taking the set $G = \{(x, y) \in X \times Y | \phi(x, y)\}$, which exists by $\Delta_0$ separation. Then the first projection $(x, y) \mapsto x$ is an isomorphism, since for all $x :\in X$ there is a unique pair $(a, y)$ such that $a = x$ and $\phi(a, y)$. So this is the graph of a function, which satisfies the above property.
Furthermore, recall that because ETCS satisfies the Axiom of Choice, it also satisfies classical logic in its internal logic. This means that for all $U \subseteq X$, we have $U \cup \neg U = X$. The principle of $\Delta_0$-separation and internal classical logic combine to give us $\Delta_0$-classical logic, which states that for any $\Delta_0$ statement $P$, $P \lor \neg P$. For $P$ can be viewed as a statement with the (unused) free variable $x :\in 1$, and therefore there is some $U \in 1$ such that $U = 1$ iff $P$. Since $U \lor \neg U = 1$, it follows that $U = 1$ or $\neg U = 1$. If $U = 1$, then $P$ holds; on the other hand, if $\neg U = 1$ then $U = 0$ and hence $U \neq 1$; then $\neg P$ holds. Note that we can allow $P$ to contain quantifiers over arrow variables as well since we can still apply $\Delta_0$-separation by the above remark.
Given $x \in X$ and $S :\in P(X)$, we write $x \in_X S$ for the proposition that $x$ is in the subobject classified by $S$. This is slightly abusive, since technically we only have a function $\in_X : X \times P(X) \to \Omega$, so the statement should generally be interpreted as $\in_X (x, s) = \top$. It's easy to show that a subset $S :\in P(X)$ is uniquely determined by $\{x \in X| x \in_X S\}$, since the latter is exactly the subobject classified by $S$.
Now consider some set $X$ which is Dedekind-infinite - that is, for which all monics $f : X \to X$ are isomorphisms. Let us consider $P(X)$, and let us note that $\forall s :\in P(X)$, either $\exists x :\in X (x \in_X s)$ or $\neg (\exists x :\in X (x \in_X s)$ (by $\Delta_0$ classical logic). And clearly, if there is no $x :\in X$ such that $x \in_X s$, then $s = 0^\#$. Now consider the map $g : \{(x, s) :\in X \times P(X) | x \in_X s\} \coprod 1 \to P(X)$ defined by $g(x, s) = s$ and $g(*) = 0^\#$. By the above remark, $g$ is epi.
We must pause here to consider the natural numbers object $\mathbb{N}$. Consider some subobject $U \subseteq \mathbb{N}$. Then we see that $U = \mathbb{N}$ if and only if $z \in U$ and for all $n :\in \mathbb{N}, n \in U \implies s(n) \in U$. For the latter means precisely that $s^{-1}(U) \subseteq U$, so that the map $s|_U : U \to \mathbb{N}$ factors through $U$. Hence, we can use the definition of the natural numbers object to come up with an inverse map $\mathbb{N} \to U$, which proves that $U = \mathbb{N}$.
Note that we can combine the above with $\Delta_0$-separation to get $\Delta_0$ induction, which states that for any $\Delta_0$ formula $\phi(x)$ with $x :\in \mathbb{N}$, if $\phi(z)$ and $\forall n :\in \mathbb{N}, \phi(n) \implies \phi(s(n))$ then for all $n$, $\phi(n)$. This follows by first constructing the subset $\{n :\in \mathbb{N} | \phi(n)\}$ using $\Delta_0$ separation.
Now let $h : P(X) \to \{(x, s) :\in X \times P(X) | x \in_X s\} \coprod 1$ be a section of $g$ (that is, such that $g \circ f = 1$).
Now given some $S :\in P(X)$ and $x \in X$, we can define $S \setminus \{x\}$ as the unique $G :\in P(X)$ such that for all $y :\in X$, $y \in_X G$ iff $y \in_X S$ and $y \neq x$. Such a $G$ exists since $\Delta_0$ separation gives us a set $\{y :\in X | y \in_X S \land y \neq x\}$, which is classified by $G$. So by $\Delta_0$ function definition, we may define a function $remove : P(X) \times X$ such that $remove(S, x) = S \setminus \{x\}$ for all $(S, x) :\in P(X) \times X$.
Now we define $u : \mathbb{N} \to P(X)$ such that $u(z) = 1^\#$ and $u \circ s = (remove \circ p_1 \coprod 0^\#) \circ h \circ u$.
We also define $getElement : P(S) \to S \coprod 1$ by $getElement = (p_0 \coprod 1) \circ h$, and we define $f : \mathbb{N} \to X \coprod 1$ by $f = getElement \circ u$. We say that $f(y)$ is defined if $f(y)$ factors through $inl : X \to X \coprod 1$ and is not defined if it factors through $inr : 1 \to X \coprod 1$. If we have $f(y) = inl(s)$, we abusively write $f(y) = s$. In general, the proposition $f(y) = s$ means $inl(s) = f(y)$ - that is, $f(y)$ is defined and $f(y)$ equals $s$.
OP has already defined $+$ and $<$, so we will proceed with those definitions. I claim that for all $n :\in \mathbb{N}$, for all $x \in X$, either there exists $m < n$ such that $f(m)$ is defined and $f(m) = x$, or $x \in_X u(n)$, but not both. This follows by induction on $n$. In the base case of $n = z$, we note that there is no $m < n$ at all. But clearly, we see that $x \in_X 1^\#$ since $1^\#$ classifies the subobject $X \subseteq X$.
Now suppose the above holds true for $k :\in \mathbb{N}$. We consider two cases. The first is that $\exists y :\in X (y \in_X k)$. In this case, we see that we are going to have $u(s(k)) = remove(u(k)_, y)$ for some $y$. In fact, it's easy to see from the definitions that the $y$ in question is exactly $f(k)$. Let us consider an arbitrary $x :\in X$. Then we see that $x \in_X u(s(k))$ iff $x \in remove(u(k), y)$ iff $x \in_X u(k)$ and $x \neq y$. Now if there is some $m < k$ such that $x = f(m)$, then clearly $m < s(k)$. And in this case, we see that $x \notin_X u(k)$, and hence $x \notin_X u(s(k))$. On the other hand, if $x \in u(k)$, then we consider two cases. By $\Delta_0$ LEM, either $x = y$ or $x \neq y$. If $x = y$, then $x = f(k)$ and $k < s(k)$. And in this case, we see that $x \notin_X u(s(k))$. And if $x \neq k$, then we see that for all $m < s(k)$, either $m = k$ (in which case $x \neq y = f(k)$ or $m < k$, in which case $x \neq f(m)$. And we see that $x \in_X u(k)$ and $x \neq y$, so $x \in u(s(k))$.
Finally, I claim that $f$ is injective where it is defined. For suppose that $f(x) = f(y)$ (both sides being defined) and $x \neq y$ for some $x, y \in \mathbb{N}$. WLOG, say that $x < y$. Then we see that $f(y) \notin u(y)$. But by the construction of $f$, $f(y) \in u(y)$ whenever $f(y)$ is defined. So this is impossible.
Now suppose that $f$ is total - that is, $\forall n$, $f(n)$ is defined. In that case, we formally have a map $f' : \mathbb{N} \to X$ such that $f = inl \circ f'$. Since $f$ is injective where it is defined, we see that $f'$ is injective on elements, hence monic. Let $U \subseteq X$ be the complementary subobject of $\mathbb{N}$. Then $X = \mathbb{N} \coprod U$. So now define a function $k : X \to X$ by defining $k(n) = s(n)$ for $n \in \mathbb{N}$, and $k(u) = u$ for $u \in U$.
I claim that $k$ is injective. For consider two elements $a :\in X$ and $b :\in X$ such that $k(a) = k(b)$. We divide the situation into four cases. The first is $a \in \mathbb{N}, b \in \mathbb{N}$. In this case, we have $s(a) = k(a) = k(b) = s(b)$, hence $a = b$ (since $s$ is monic). The second case is $a \in U, b \in U$. In this case, we have $a = k(a) = k(b) = b$. The third case is $a \in \mathbb{N}$, $b \in U$. In this case, $k(a) \in \mathbb{N}$ and $k(b) \in U$, so they cannot be equal since $U \cap \mathbb{N} = 0$ by the definition of complement. The four case is $a \in U, b \in \mathbb{N}$ which is analogous to the previous case.
But I also claim that $k$ is not surjective. For suppose given some $y :\in X$ such that $k(y) = z$. Either $y \in \mathbb{N}$ or $y \in U$. If $y \in \mathbb{N}$ then we have $s(y) = z$, but we know that $\forall y :\in \mathbb{N} (s(y) \neq z)$. And if $y \in U$, then $k(y) \in U$ and $k(y) = z \in \mathbb{N}$, so $k(y) \in U \cap \mathbb{N} = 0$; contradiction.
So we have a monic which is not epic. This is a contradiction.
Therefore, $f$ must not be total; that is, it is not the case that $\forall n \in \mathbb{N}, f(n)$ is defined. So there must exist some $n :\in \mathbb{N}$ for which $f(n)$ is not defined (using $\Delta_0$ classical logic on the statement $\exists n \in \mathbb{N} (f(n)$ is undefined$)$ and keeping in mind that ``$f(n)$ is undefined'' is shorthand for $f(n) = inr(*)$, where $*$ is the unique element of 1).
Now take the smallest $n :\in \mathbb{N}$ such that $f(n)$ is undefined (this exists using the well-ordering principle). Then clearly, $f$ is defined for all $m < n$. Since $f(n)$ is undefined, this means that $u(n)$ must be empty.
So consider the subobject $S = \{m :\in \mathbb{N} | m < n\} \subseteq \mathbb{N}$, and define $f' : S \to X$ using the fact that $f$ is defined on $S$. Then $f'$ is monic, since $f$ is injective where it is defined. And I claim that $f'$ is also surjective. For consider some $x \in X$. Then either $x \in_X u(n)$ or there exists some $m < n$ such that $f'(m) = x$. But we know that $x \notin_X u(n)$ since $u(n) = 0^\#$.
Thus, we see that for every Dedekind-finite object $X$, there exists a (necessarily unique) $n :\in \mathbb{N}$, such that $\{m :\in \mathbb{N} | m < n\}$ is isomorphic to $X$.
Let's consider the situation in a topos $T$ with natural numbers object which does not necessarily model ETCS@. If this topos satisfies the internal axiom of choice, then the above proof is valid in the stack semantics of $T$. That is, $1 \Vdash$ \textopencorner For every Dedekind-finite object $X$, there exists a unique $n :\in \mathbb{N}$ such that $X$ and $\{m :\in \mathbb{N} | m < n\}$ are isomorphic \textcorner. For more details on the Stack Semantics, consult Mike Shulman's paper on material set theories and the stack semantics on arXiv.
Interpreting the stack semantics, this states that in any topos satisfying the axiom of choice and having a NNO, if $X$ is an internal Dedekind-finite object, then there is some $n :\in \mathbb{N}$ such that $X$ is internally isomorphic to $\{m \in \mathbb{N} | m < n\}$ (that is, the internal logic states there is an isomorphism, but there may not actually be an isomorphism). Formally, the ``internal isomorphism condition'' states that there is some epimorphism $f : A \to 1$ and some isomorphism $A \times X \to A \times \{m \in \mathbb{N} | m < n\}$ in the slice category $T/A$. An internal Dedekind-finite object is an object $X$ such that for all objects $A$ and all monics $f : A \times X \to A \times X$ in $T/A$, $f$ is an isomorphism.
If $1$ is an externally projective object (for example, when $T$ satisfies the external axiom of choice), this means that there actually does exist an isomorphism between $X$ and $\{m :\in \mathbb{N} | m < n\}$.
An example of an object which is internally isomorphic to $\{m \in \mathbb{N} | m < n\}$ but not actually isomorphic would be the sheaf of sections of the projection map $\mathbb{S}_1 \to \mathbb{R}P_1$, which is internally isomorphic to the sheaf of sections of $\{0, 1\} \times \mathbb{R}P_1$ because there are locally 2 sections but not externally since the two have different fundamental groups. This isn't a great example since the category of sheaves on $\mathbb{R}P_1$ doesn't satisfy internal choice, but it's at least illustrative of the possibility.
Edit:
Here is a completion of OP's proof. It uses tikz-cd diagrams, so I can't directly copy and paste the TeX here. I will add this to my answer properly at some point.