<s>[INST] Proving $abcd \le 3+ ab+ac+ad+bc+bd+cd$ when $(a^2+1)(b^2+1)(c^2+1)(d^2+1)=16$ Mathematica proves the inequality (the code on demand) $$abcd \le 3+ ab+ac+ad+bc+bd+cd$$ under the condition $$(a^2+1)(b^2+1)(c^2+1)(d^2+1)=16$$ 
The equality is attained at 
$$\begin{align}
a &=\frac{\frac{927}{512}-\frac{73 \left(1196032-\sqrt{578562030719}\right)}{83867680}}{-\frac{609 \left(1196032-\sqrt{578562030719}\right)}{1341882880}+\frac{\sqrt{578562030719}-1196032}{2620865}+\frac{73}{32}} \\[4pt]
b &= -\frac{87}{32} \\[4pt]
c &= \frac{7}{16} \\[4pt]
d &= \frac{1196032-\sqrt{578562030719}}{2620865}
\end{align}$$

The question arises: How to prove it by hand?

 [/INST] Since $$(x^2+y^2)(z^2+t^2)=(xz+yt)^2+(xt-yz)^2,$$ we obtain:$$16=(a^2+1)(b^2+1)(c^2+1)(d^2+1)=((ab-1)^2+(a+b)^2)((cd-1)^2+(c+d)^2)=$$
$$=((ab-1)(cd-1)-(a+b)(c+d))^2+((ab-1)(c+d)+(cd-1)(a+b))^2=$$
$$=(1+abcd-ab-ac-ad-bc-bd-cd)^2+$$
$$+(abc+abd+acd+bcd-a-b-c-d)^2\geq$$
$$\geq(abcd+1-ab-ac-ad-bc-bd-cd)^2,$$ which gives
$$-4\leq abcd+1-ab-ac-ad-bc-bd-cd\leq4$$ and
$$3+ab+ac+ad+bc+bd+cd\geq abcd.$$
The equality occurs for $$abc+abd+acd+bcd=a+b+c+d$$ and $$\prod_{cyc}(a^2+1)=16.$$
</s>