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?
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.$$