Yes, this works in this particular instance, but I was thinking more of a general case. Suppose one wants to have a function with two arguments (for concreteness, let's say the two arguments are both mathematical expressions in one real/complex variable) which would return True if the two expressions are equivalent and False otherwise, similar to how an auto-grader would attempt to determine if two arbitrary pieces of code are equivalent. How could one go about writing a function like this in Mathematica?
I find it a little puzzling how Mathematica treats certain mathematical expressions. For example,
Sin[ArcTan[x]]//FullForm
produces
Times[x,Power[Plus[1,Power[x,2]],Rational[-1,2]]]
and
Sin[ArcTan[x]+Pi/2] //FullForm
produces
Power[Plus[1,Power[x,2]],Rational[-1,2]]
so some identities are built-in in FullForm and in how Mathematica treats the expressions. These examples lead one to expect that Sin[ArcTan[x]+Pi/4] //FullForm will be Times[Power[2,Rational[-1,2]],Plus[1,x],Power[Plus[1,Power[x,2]],Rational[-1,2]]]
but instead one gets Sin[Plus[Times[Rational[1,4],Pi],ArcTan[x]]].
Both, Expand and Simplify leave Sin[ArcTan[x]+Pi/4] unchanged and the suggested approaches do not work for verifying that Sin[Plus[Times[Rational[1,4],Pi],ArcTan[x]]] and Times[Power[2,Rational[-1,2]],Plus[1,x],Power[Plus[1,Power[x,2]],Rational[-1,2]]] are equivalent.