I'm trying to find a simple proof that a monoid under Day convolution is equivalent to a lax monoidal functor (see nCatLab). For simplicity, consider functors from $C$ to $Set$. For $F$ to be a monoid there has to be a natural transformation:
$ \mu : F \otimes F \to F $
where the tensor product is the Day convolution:
$F\otimes F := \int^{x y} C(x \otimes y, -) \times F(x) \times F(y)$
A lax monoidal functor has a natural transformation:
$F(x) \times F(y) \to F(x \otimes y)$
which we can plug in to get:
$\int^{x y} C(x \otimes y, -) \times F(x \otimes y)$
If I could only make a "change of variables" from $(x, y)$ to $x\otimes y$, like this:
$\int^{x \otimes y} C(x \otimes y, -) \times F(x \otimes y)$
I could use the ninja Yoneda lemma to perform the integral and get $F$. How do I convert this handwaving argument to a proof?