One important example is the equivalence of standard bottom-up induction and top-down induction. It is interesting that bottom-up induction does not extend immediately to ordinals (since successors and limits must be handled differently), while top-down induction extends without any change. On the other hand, top-down induction is usually easier to learn without error, especially in the form of structural induction (see this explanation).
Closely related is the equivalence of induction and well-ordering. Here there is an interesting disparity, because in some cases considering the smallest counter-example with sizes from some well-order yields much easier proofs, partly because it is essentially induction wrapped in a non-constructive proof by contradiction, which is in some sense strictly stronger than constructive induction, namely when in a constructive logic. This may seem irrelevant, but in many cases it is far easier to see a proof by well-ordering (also called extremal principle) than to see the equivalent proof by induction (see this short list on AOPS.
For analysis in particular, it's interesting to look at the proofs of basic results such as that continuous functions on a compact set are bounded and attains its extrema, and are uniformly continuous. Because of the equivalent notions of compactness for metric spaces, it is interesting to look at the resulting differences in proofs. One would notice though that the core of each proof is pretty much the same for dimension at least 2. However, in 1 dimension there are rather different proofs that I discovered long time ago that do not extend (at least I don't see how), which I give as an example below.
There are many ways to precisely quantify sameness of proofs. One way that is good for students to learn is to see exactly where each part of the theorem and which axioms are used in the proof, and also count the number of times each of them is used. Two proofs are essentially the same when they are minimal in that respect and use each part the same number of times. This can be done at any level of detail, but usually we do not include any of the logical axioms except for double negation elimination (equivalently proof by contradiction in the form "$\neg P \rightarrow \bot \vdash P$"), and often we work over a specific axiomatization such as that of the real numbers (second-order completeness). Here is an example:
$\def\rr{\mathbb{R}}$
$\def\less{\smallsetminus}$
Any continuous function $f : [0,1] \to \rr$ is bounded on $[0,1]$.
Proof [with reason on the right of each line]:
Take any continuous function $f : [0,1] \to \rr$. [logically necessary]
Let $S = \Big\{ p : p \in [0,1] \land \text{$f$ is bounded on $[0,p]$} \Big\}$. [by comprehension]
Then $0 \in S$ because $\forall x \in [0,0]\ ( |f(x)| \le |f(0)| )$. [this uses the left endpoint of $[0,1]$]
Then $S$ is non-empty. [by definition of non-empty]
Also, for any $p \in S$, we have $p \le 1$ by construction of $S$. [this uses the right endpoint of $[0,1]$]
Thus $S$ has a least upper bound $c$ in $\rr$. [by completeness of real numbers]
Firstly $c \ge 0$ because $0 \in S$. [this uses that $c$ is an upper bound]
Secondly $c \le 1$ because $1$ is an upper bound for $S$ in $\rr$. [this uses that $c$ is the least one]
Let $δ > 0$ such that, for any $x \in [0,1]$, if $|x-c| \le δ$ then $|f(x)-f(c)| \le 1$. [this uses continuity but is much weaker (*)]
Thus $f$ is bounded on $[0,1] \cap [c-δ,c+δ]$ by $|f(c)|+1$. [by triangle inequality]
Also $f$ is bounded on $[0,c-δ]$ by definition of $S$. [this is why we defined $S$ like that]
Thus $f$ is bounded on $[0,1] \cap [0,c+δ]$. [by basic properties of reals]
Thus $\min(1,c+δ) \in S$ by definition of S. [in the reverse direction]
Thus $\min(1,c+δ) \le c$ and hence $1 \le c$. [by basic properties of reals]
Therefore $f$ is bounded on $[0,1]$ since $[0,1] \subseteq [0,c+δ]$.
(*) This is a clear example of an important point that students should learn to identify and understand. Continuity of $f$ is essentially an assertion of the form "$\forall ε > 0\ ( \text{$f$ is $ε$-continuous} )$", and here all we used was $1$-continuity of $f$, and $1$ was arbitrary except that it was more than $0$. Students with a proper foundation in logic would not only be able to prove the theorem but also realize via this observation that we can strengthen it to:
Given any $ε > 0$, any $ε$-continuous function $f : [0,1] \to \rr$ is bounded on $[0,1]$.
Notice that in the above proof every part of the theorem statement has been used exactly once. It is instructive to check that dropping any single part, such as continuity of $f$, or $[0,1]$ being closed on each end, results in a false assertion. With a suitable notion of shortness, this implies that the proof is more or less minimal over the standard axiomatization of the reals, which anyone reading the proof would expect.
Note however that theorems and proofs do not live in isolation, and so one can consider any particular body $B$ of mathematics as a whole, and ask what is the shortest proof of all the theorems in $B$. This minimization tends to have all the key theorems factored out, much like in Lempel-Ziv compression. What we are minimizing is essentially the Kolmogorov complexity of $B$ with respect to the underlying formal system (such as ZFC).
For any collection $C$ of theorems over an existing body $B$ where $B$ has a minimal proof, one can look at the proof of all the theorems in $C$ over $B$. Two proofs are then reasonably considered identical if they use the same axioms and the same proven sentences in $B$. To make sure this notion coincides with our intuition, we can require that a sentence must be labelled before it can be used as a theorem, so that only major results will be labelled in a minimal proof of $B$.
If the two proofs $P,Q$ of $C$ over $B$ are not considered identical according to the above, we can measure the difference via some reasonable proof distance, such as one that I just thought of that takes into account differences between theorems used. First let $S,T$ be the collection of all theorems in $B$ that $P,Q$ respectively depend on directly. Then let $R$ be a minimal proof of $S \cup T$. (Give each equal weight if there is more than one.) Then the proof distance between $P,Q$ is the edit distance between theorems and axioms used in $P$ and $Q$ ignoring order, plus the total length of the segments of $R$ that are used only for one of $S,T$. This definition ensures that two proofs that have the same essential ingredients have small proof distance, and proof distance is only slightly affected if the same theorem is proven and used under different names, since minimizing the proof of $S \cup T$ automatically finds the common ingredients.
Likewise, and in fact more easily, we can define similarity in mathematical content of theorems. Given any two collections $A,B$ of theorems, let $R$ be a minimal proof of $A \cup B$. Then the content distance between $A$ and $B$ is just the total length of the segments of $R$ that are used only for one of $A,B$.
This is quite technical, but I believe it quite accurately captures what we mean when we say things like "Compactness and completeness are essentially equivalent theorems about first-order logic.". Of course all true assertions are equivalent, including "$0 = 0$.", but we all know that the statement is trying to say that the easiest way to prove both compactness and completeness is to prove one and then derive the other as a corollary. Indeed if we let $A$ be the singleton containing "compactness" and $B$ be the singleton containing "completeness", then since there is a short proof of $A$ over $B$ and of $B$ over $A$, the shortest proof of $A \cup B$ is thus only a few lines longer than the common ingredients of the individual proofs, and thus there is negligible content difference between compactness and completeness, as expected.