Let #2tan^-1(1/5)+tan^-1(1/7)+2tan^-1(1/8)=a#
Let #theta=tan^-1(1/5)# and #phi=tan^-1(1/7)# and #psi=tan^-1(1/8)#
Then #tantheta=1/5# and #tanphi=1/7# and #tanpsi=1/8#
#costheta=sqrt(1/(1+tan^2theta))=5/sqrt26#
#sintheta=sqrt(1-cos^2theta)=1/sqrt26#
#cosphi=sqrt(1/(1+tan^2phi))=7/sqrt50#
#sinphi=sqrt(1-cos^2phi)=1/sqrt50#
#cospsi=sqrt(1/(1+tan^2psi))=8/sqrt65#
#sinpsi=sqrt(1-cos^2psi)=1/sqrt65#
#2theta+phi+2psi=a#
Let #rho=2theta+2psi#
#phi+rho=a#
#sin(phi+rho)=sina#
#sin(phi+rho)#
#=sinphicosrho+cosphisinrho#
#=sinphi[cos(2theta+2psi)]+cosphi[sin(2theta+2psi)]#
#=sinphi(cos2thetacos2psi-sin2thetasin2psi)+cosphi(sin2thetacos2psi+cos2thetasin2psi)#
#=sinphi[(2cos^2theta-1)(2cos^2psi-1)-(2sinthetacostheta)(2sinpsicospsi)] + cosphi[(2sinthetacostheta)(2cos^2psi-1)+(2cos^2theta-1)(2sinpsicospsi)]#
#=1/sqrt50[(2(5/sqrt26)^2-1)(2(8/sqrt65)^2-1)-(2(1/sqrt26)(5/sqrt26))(2(1/sqrt65)(8/sqrt65))]#
#+7/sqrt50[(2(1/sqrt26)(5/sqrt26)(2(8/sqrt65)^2-1)+(2(5/sqrt26)^2-1)(2(1/sqrt65)(8/sqrt65))]=sqrt2/2#
#sin(phi+rho)=sina=sqrt2/2#
#phi+rho=a=pi/4+2kpi, k in ZZ#
#2theta+phi+2psi=a=pi/4+2kpi, k in ZZ#
# 0 < tantheta,tanphi,tanpsi < 1#
#therefore 0 < theta,phi,psi < pi/4#
#therefore 0 < 2theta+phi+2psi < (5pi)/4#
#therefore2theta+phi+2psi=pi/4#
#thereforea=pi/4#
#therefore2tan^-1(1/5)+tan^-1(1/7)+2tan^-1(1/8)=pi/4# #sf(QED)#