Monoidal functor from preserves limits/colimits

Stream: Is there code for X?

[Jack J Garzella]

Say we have a functor $\mathcal{F} : C \to D$. I'm trying to deduce that various functors are lax monoidal from the fact that they preserve limits, given that both monoidal categories in question $C$ and $D$ are defined such that the tensor and the identity are defined using limits, i.e. monoidal_of_has_finite_proudcts or monoidal_of_chosen_finite_products.

Is there code in mathlib that does this? If not, how would I attempt to state a lemma that captures this?

Side notes:
*Though I only need to show that such functors are lax monoidal, they are in fact monoidal functors, so it might be nice to also show this.
*Eventually, I'll want to do the same thing but with monoidal categories whose monoidal structures are colimits, like e.g. $R$-modules with tensor product.