Is A∨¬A a tautology when there is a proof (by contradiction)? $A \lor \neg A$ is stated as a "tautology", but is it really a tautology? It can be proven by counterposition. And therefore it is not a tautology when it can be proven(?)
Update
Here's the proof (by contradiction) I mean:
¬(A∨¬A) (assumption)
   A      (assumption)
   A∨¬A  (rule of introduction)
  人      (contradiction)
 ¬A
 A∨¬A   (rule of introduction)
 人      (contradiction)
¬¬(A∨¬A)
A∨¬A

 A: Part of the problem here may be that "tautology" has a far more specific meaning in mathematical logic than in ordinary usage.  The more specific meaning is "a statement S that always true, solely on the basis of how S is constructed from smaller statements by means of propositional connectives and the meanings (truth tables) of the connectives".  So $A\lor\neg A$ is a tautology because it is true solely because of the meanings of $\lor$ and $\neg$.  But $1=1$ is not a tautology because its truth depends on the meaning of $=$, which is not a propositional connective.  Similarly, if $P$ is a unary predicate, then $P(a)\to(\exists x)\,P(x)$, though logically valid, is not a tautology because its validity depends on the meanings of both $\to$ and $\exists$, the latter of which is not a propositional connective.
In ordinary, non-technical usage, "tautology" means (according to my dictionary) saying the same thing in different words; I've heard it used more generally to mean anything that is obviously true.  So all of the examples in my first paragraph would be tautologies in this sense.
A: Try constructing a truth table and you will see that it is in fact a tautology.
A: $A\vee \neg A$ is a tautology in classical (i.e., Aristotelian) logic because you can prove that using the deduction rules of the classical proposition calculus no matter what the truth value of $A$ is, the truth value of $A\vee \neg A$ is always true. That is the meaning of tautology. 
In non-classical logical systems, such as intuitionism or constructivism, $A \vee \neg A$ is not a tautology. There the interpretation of $P \vee Q$ is not "either P or Q is true" but rather the more constructive "Either I have a proof of P or I have a proof of Q". A famous example to illustrate this is the following: Theorem: There exist two irrational numbers $a,b$ such that $a^b$ is rational. A classical proof can go like this: if $\sqrt2 ^\sqrt2$ is rational we are done. Else, consider $(\sqrt2^{\sqrt2})^{\sqrt2}=\sqrt2^2=2$, a rational. Classically this finishes the proof but constructively it is not a valid proof since it does not actually show which one of the two candidates works. 
A: The OP wants to know if a proposition such as $A \lor \lnot A$ is a tautology if it can be proven. The OP provided a proof so the answer depends on the definition of tautology. Here is Wikipedia's definition:

In logic, a tautology ... is a formula or assertion that is true in every possible interpretation.

For propositional logic Wikipedia defines an interpretation as follows:

The standard kind of interpretation in this setting is a function that maps each propositional symbol to one of the truth values true and false.

Such interpretations can be illustrated with truth tables. For $A \lor \lnot A$ we have the following truth table showing that for all interpretations the proposition is true and hence the proposition is a tautology:

Since propositional logic has derivation systems that are both sound and complete.  Any tautology can be derived in such systems because they are complete. Any derivation in such systems can be formatted as a tautology in a truth table because they are sound. 
For example, given the premises $P$, $P \implies Q$ one can derive $Q$. If one conjoins the premises and connects these conjoined premises and the conclusion with a conditional symbol, one can see from a truth table that it will also be a tautology.  For this example, here is the truth table:

One should expect to be able to derive any tautology in propositional logic in a sound and complete derivation system for propositional logic.

Michael Rieppel. Truth Table Generator. https://mrieppel.net/prog/truthtable.html
Wikipedia contributors. (2019, April 30). Interpretation (logic). In Wikipedia, The Free Encyclopedia. Retrieved 12:30, August 6, 2019, from https://en.wikipedia.org/w/index.php?title=Interpretation_(logic)&oldid=894912837
Wikipedia contributors. (2019, June 21). Tautology (logic). In Wikipedia, The Free Encyclopedia. Retrieved 12:15, August 6, 2019, from https://en.wikipedia.org/w/index.php?title=Tautology_(logic)&oldid=902843519
