This seems obvious to me, but do we need a formal proof to establish this is always true?
Let $x$ and $y$ be irrational numbers with decimal representations
$x = 0.x_1x_2x_3 \dots$
$y = 0.y_1y_2y_3 \dots$
If $x_n = y_n$ for $n \in \mathbb{N}$
Can we then infer that $x = y$ ?
Perhaps it seems obvious to you because the symbols would be identical. But a real number is not a symbol, it is an abstract mathematical quantity.
So if you are defining the real numbers by a construction (Dedekind cuts; or equivalence classes of Cauchy sequences of rational numbers), or if on the other hand you are starting from axioms (the axioms for a complete ordered field), there is indeed something to prove.
What a decimal number really is, is just a shortand for a certain infinite series: $$0.x_1x_2x_3\cdots = \sum_{n=1}^\infty \frac{x_n}{10^n} $$ So you will need at some point to prove a theorem which says that if an infinite series converges then the number it converges to is unique.