The identity $\tan({\pi\over4}-{a\over2}) = \sec(a)-\tan(a)$

Today I was solving an exercise and while checking the solution on WolframAlpha, the website used the following identity: $$\tan \left({\pi\over4}-{\alpha\over2} \right) = \sec(\alpha)-\tan(\alpha)$$ Since I've never seen that formula, I tried to calculate it with the identities I know, especially using $$\tan \left({\pi\over4}-{\alpha\over2} \right) = {(1-\tan({\alpha\over2}))\over(1+\tan({\alpha\over2}))},$$ but I couldn't make it work.

Is this a known property of trigonometry, like for example $\cos({\pi\over2}-x)=\sin(x)$?

Denote $\tan(\alpha/2)=t$. Then $$ \sin \alpha = \dfrac{2t}{1+t^2}, \quad \cos \alpha = \dfrac{1-t^2}{1+t^2}, \quad \tan \alpha = \dfrac{2t}{1-t^2}. $$ Then $$ \tan\left(\frac{\pi}{4}-\frac{\alpha}{2}\right) = \dfrac{1-t}{1+t} = \dfrac{(1-t)(1-t)}{(1+t)(1-t)} = \dfrac{(1+t^2)-2t}{1-t^2} $$ $$ = \dfrac{1+t^2}{1-t^2} - \dfrac{2t}{1-t^2} = \frac{1}{\cos \alpha} - \tan \alpha $$ $$ =\sec\alpha - \tan\alpha. $$

The identity $$ \sec x \pm \tan x = \tan\left( \frac \pi 4 \pm \frac x 2 \right) $$ is one that I sometimes think of as the "cartographers' tangent half-angle formula" because of the way in which it arises in the theory of the Mercator projection, i.e. in finding the antiderivative of the secant function. The desire to find the antiderivative of the secant function came from its application to cartography in the late 1500s and early 1600s.

Recall that $\sec(\pm x) = \sec x$ and $\tan(\pm x)=\pm\tan x$, so when the sign of $x$ changes, the sign of $\tan x$ changes but that of $\sec x$ does not. Or in other words, secant is even and tangent is odd.

Since $x$ appears on the right side only in $\dfrac x 2$, and on the right side without such a fraction, you should expect to either prove a half-angle formula or rely on one that's already proved. Recall that $$ \tan \frac x 2 = \frac{\sin x}{1+\cos x}. $$ So \begin{align} & \tan\left( \frac \pi 4 \pm \frac x 2 \right) = \frac{\sin\left( \frac \pi 2 \pm x \right)}{1+\cos\left(\frac\pi2 \pm x\right)} = \frac{\cos x}{1\mp \sin x} = \frac{(\cos x)(1\pm\sin x)}{(1\mp\sin x)(1\pm\sin x)} \\[10pt] = {} & \frac{(\cos x)(1\pm\sin x)}{1-\sin^2 x} = \frac{(\cos x)(1\pm\sin^2 x)}{\cos^2 x} = \frac{1\pm\sin x}{\cos x} = \frac 1 {\cos x} \pm \frac{\sin x}{\cos x} \\[10pt] = {} & \sec x \pm \tan x. \end{align}

Here's a couple of trigonographs:

$$\begin{align} \sec\theta - \tan\theta \;=\; \tan\phi \;=\; \tan\frac{90^\circ - \theta}{2} \;=\; \tan\left( 45^\circ - \frac{\theta}{2}\;\right) \\[4pt] \sec\theta + \tan\theta \;=\; \tan\psi \;=\; \tan\frac{90^\circ + \theta}{2} \;=\; \tan\left( 45^\circ + \frac{\theta}{2}\;\right) \end{align}$$

Yes.

Wikipedia states $$\tan x + \sec x = \tan\left(\frac{x}{2}+\frac{\pi}{4}\right)$$ Re-arranging, we solve for $\sec x$: $$\sec x = \tan\left(\frac{x}{2}+\frac{\pi}{4}\right) - \tan x = \overbrace{\tan x + \tan\left(\frac{\pi}{4}-\frac{x}{2}\right)}^{\text{Your identity}}$$ We know that because $\tan x$ is an odd function, $$\tan (-x) = - \tan x \to \tan\left(\frac{x}{2}-\frac{\pi}{4}\right)=-\tan\left(\frac{\pi}{4}-\frac{x}{2}\right)$$ It should then be possible to prove your identity, via only a few more steps: $$\tan\left(\frac{x}{2}+\frac{\pi}{4}\right)+\tan\left(\frac{x}{2}-\frac{\pi}{4}\right)=2\tan x$$

The identity also pops up in Cayley's explanation of the integral of $\sec x$.