However, suppose I proved $p$ to be true. I am tempted to write $p \iff \top$, but this means "$p$ is a tautology".
No it doesn't. $p \Leftrightarrow \top$ is just another formula, one that happens to be true in exactly the same structures as $p$ is.
It also happens that $p \Leftrightarrow \top$ is a tautology exactly if $p$ itself is a tautology. So if you write, "$p\Leftrightarrow\top$ is a tautology", you're also implicitly asserting that $p$ is a tautology.
But simply writing "$p\Leftrightarrow \top$", without further, is either just putting the formula on the table for further study at the metalevel, or implicitly an assertion that "$p\Leftrightarrow \top$" happens to be true under a particular intended interpretation of the symbols -- even though we're often leaving it implicit what the intended interpretation means.
If you want to say that $p$ is a tautology, then you need to say "$p$ is a tautology"; there is no generally understood symbolic way of saying that. You can say, at the metalevel,
$$ \vDash p $$
which asserts that $p$ is logically valid, and in some presentations "tautology" is used to mean "logically valid". With the definition you quote, however, that is not the case.
A formula $A$ is a tautology if it is true with every assignment.
A formula $A$ is satisfiable if there is at least an assignemnt $v$ such that $A$ is true for $v$.
If $A$ is true for the assignment $v$, then its negation, $¬A$, is false for that assignment.
A formula $A$ is a tautology iff its negation, $¬A$, is not satisfiable.
The complement of a decision problem :
is the decision problem resulting from reversing the yes and no answers.
Thus, in a nutshell, if the answer to the problem "is $A$ in TAUT ?" is NO, then $¬A$ is in SAT.
More precisely, the problem of determining if some formula $A$ is not a tautology is thus equivalent to the problem of determining if the negation of the formula, $¬A$, is satisfiable.
It seems to me that it is only a terminological issue. Compare with :
Now we define some additional complexity classes related to $\text {P}$ and $\text {NP}$.
If $L ⊆ \{ 0, 1 \}^∗$ is a language, then we denote by $\overline L$ the complement of $L$.
We make the following definition: $\text {coNP} = \{ L \mid \overline L ∈ \text {NP} \}$.
$\text {coNP}$ is not the complement of the class $\text {NP}$. The following
is an example of a $\text {coNP}$ language: $\overline {\text {SAT} } = \{ \varphi \mid \varphi \text { is not satisfiable} \}$.
The decision problems (or languages) are complementary : not the corresponding classes of formulae.
Best Answer
You have to check the definition of tautology.
Usually, tautology is defined in the context of propositional logic.
For first order logic, a formula is a tautology if it is a formula obtainable from a tautology of propositional logic by replacing (uniformly) each sentence symbol by a formula of the first-order language.
Thus, $\forall x P(x) \to \forall x P(x)$ is a tautology, being an "instance" of $A \to A$, while $x=x$ is not, because it is an "instance" of the single sentence symbol $A$, which is not a tautology.
Of course, $x=x$ is valid, i.e. true in every interpretation.