That’s logic, not field theory.
Yeah, I was actually guessing it would be something like that. I imagine what you did was either defining equality of sets extensionally (“X = Y” meaning “X and Y have the same elements”) or decategorifying into cardinalities (“X = Y” meaning “There is a bijection between X and Y”) and then proving reflexivity for the defined equality relation (which is pretty trivial, but not necessarily axiomatic, per se, as it generally would be for equality taken as a logical primitive).
Proving such trivial things is even far less complicated than proving 2^(1/2) is irrational, though (except possibly for getting obscured in unfamiliar formalization). The most complicated sort of situation I can imagine in which one would be “proving the reflexivity of equality” is when one defines equality by structural recursion, and then proves reflexivity by structural induction. For example, in the context of systems like Peano Arithmetic, we could choose to not take = as a logical primitive, but rather define it via the following axioms:
0 = 0
not (0 = Sx)
Sx = Sy iff x = y
Then we’d have to appeal to a simple induction to show the reflexivity of this defined equality. That’s probably as complicated as it gets.