I understood the question being about the "mixing variables" technique, not about proving the lemma. While I haven't heard the term, the technique itself is familiar, though I could rarely apply it in an olympiad setting.
Using the lemma on $(a,b), (a,c)$ and $(b,c)$ and multiplying the result we get
$$(a^2+1)^2(b^2+1)^2(c^2+1)^2 \le \left(\left(\frac{a+b}2\right)^2+1\right)^2\left(\left(\frac{a+c}2\right)^2+1\right)^2\left(\left(\frac{b+c}2\right)^2+1\right)^2.$$
Notice that the term on the right has the same form as the term on the left. Let's shorten this with
$$f(x,y,z)=(x^2+1)^2(y^2+1)^2(z^2+1)^2.$$
and the above inequality simply becomes
$$f(a,b,c) \le f(\frac{a+b}2, \frac{a+c}2,\frac{b+c}2).$$
Once we've established that $\frac{a+b}2,\frac{a+c}2$ and $\frac{b+c}2$ also fulfill the property that any product of 2 (distinct) of them is at least $1$ (which I'll do below to not disturb the flow of the argument), we can apply the above inequality again, using $a'=\frac{a+b}2,b'=\frac{a+c}2, c'=\frac{b+c}2$:
$$f(a,b,c) \le f(\frac{a+b}2, \frac{a+c}2,\frac{b+c}2) \le f(\frac{b+2a+c}4,\frac{a+2b+c}4,\frac{a+2c+b}4).$$
We can continue to do this, in each step increasing the RHS of the previous inequality by replacing it with function $f$ applied the the pairwise arithmetic mean of the previous arguments.
The important part is that if you take 3 numbers and repeatedly replace them with their pairwise arithmetic mean, you get a series of tuples that converges on their "3-way" arithmetic mean. That can be seen by noticing that the sum of elements for all those tuples stays the same ($a+b+c$) and the difference between highest and lowest element is halved in each step.
So we have a series of inequalities $f(a,b,c) \le f(a_1,b_1,c_1) \le f(a_2,b_2,c_2)\le \ldots$, where $\lim_{n\to\infty}a_n = \lim_{n\to\infty}b_n = \lim_{n\to\infty}c_i = {a+b+c \over 3}$.
Since $f$ is continuous, we finally get
$$f(a,b,c) \le f({a+b+c \over 3},{a+b+c \over 3},{a+b+c \over 3}),$$
which is the statement to prove in the problem, raised to the 6th power.
Now comes the proof omited above that the "min product condition" is 'inherited' from $(a,b,c)$ to $(\frac{a+b}2,\frac{a+c}2,\frac{b+c}2)$. Since the condition is symmtrical, we can assume $a \le b \le c$ w.l.o.g. We know that $ac,ab \ge 1$. The two smallest among $(\frac{a+b}2,\frac{a+c}2,\frac{b+c}2)$ are $\frac{a+b}2$ and $\frac{a+c}2$, and we get
$$\frac{a+b}2\frac{a+c}2=\frac{a^2+ac+ab+bc}4 \ge \frac{a^2+1+1+\frac1{a^2}}4 \ge 1,$$
using $b,c \ge \frac1a$ and the well known $x+\frac1x \ge 2$ for $x=a^2$.
Best Answer
(A) Proof Crux :
$\frac{a^3}{b+c+d}+\frac{b+c+d}{18}+\frac{a}{6}+\frac{1}{12} \geq \frac{2}{3}a \tag{1}$
You can think that this is AM-GM like :
$(A+B+C+D)/4 \geq \sqrt[4]{ABCD} \tag{2}$
Where : $A=\frac{a^3}{b+c+d}$
& $B=\frac{b+c+d}{18}$
& $C=\frac{a}{6}$
& $D=\frac{1}{12}$
Plug-in these values into (2) & take 4th root & move the Denominator up to get (1) & move "forwards".
(B) How did these values turn up ? What was the motivation ?
Proof requires terms with $a^3$ Numerator & $b+c+d$ Denominator Cyclically. When we want to get $a$ , eliminating the other unknowns , we can multiply by Denominator & by $a$ to then take 4th root. We also require a Constant.
Proof writer would have tried this :
$\frac{a^3}{b+c+d}+\frac{b+c+d}{k_1}+\frac{a}{k_2}+\frac{1}{k_3} \geq 4\sqrt[4]{\frac{a^3(b+c+d)a}{(b+c+d)k_1k_2k_3}} \tag{3}$
Eventually , what we want to get though (3) will then have to make :
$2/3=4/\sqrt[4]{k_1k_2k_3} \tag{4}$
Proof writer might have got various Solutions to (4) & choose this :
$(k_1,k_2,k_3)=(18,6,12) \tag{5}$
Proving the Crux uses this (5) & things work out.
Proof writer would have tried alternatives too , something like this :
$\frac{a^3}{b+c+d}+\frac{b+c+d}{k_1}+\frac{1}{k_2} \geq 3\sqrt[3]{\frac{a^3(b+c+d)}{(b+c+d)k_1k_2}} \tag{6}$
It might have worked out , though getting $(k_1,k_2)$ to satisfy (6) might have been harder , giving complicated values , hence this was not used.
That motivation is not given , we have to work "backwards" to figure out that.