\begin{tikzcd}[proof]
\beta_{(1)}\ol{g}_!\bigl(\gamma^*(c)\otimes \ol{g}^*\beta^*(b)\bigr)
\ar[d,"\beta_{(1)}\ol{g}_!(\id\otimes\tau^{-1})"']
\ar[r,"\beta_{(1)}\pf_{\ol{g}}"]
\beta_{(1)}\bigl(\ol{g}_!\gamma^*(c)\otimes\beta^*(b)\bigr)
\ar[r,"\beta_{(1)}(\phi\otimes\id)"]
\beta_{(1)}\bigl(\beta^*g_!(c)\otimes\beta^*(b)\bigr)
\ar[dd,"\beta_{(1)}\mon_\beta"]
\\
\beta_{(1)}\ol{g}_!\bigl(\gamma^*(c)\otimes\gamma^*g^*(b)\bigr)
\ar[d,"\beta_{(1)}\ol{g}_!\mon_\gamma"']
\\
\beta_{(1)}\ol{g}_!\gamma^*\bigl(c\otimes g^*(b)\bigr)
\ar[d,"l(\phi)"']
\ar[r,"\beta_{(1)}\phi"]
\ar[dr,phantom,"(B')"{font=\tiny}]
\beta_{(1)}\beta^*g_!\bigl(c\otimes g^*(b)\bigr)
\ar[d,"\varepsilon_\beta"']
\ar[r,"\beta_{(1)}\beta^*\pf_g"]
\beta_{(1)}\beta^*\bigl(g_!(c)\otimes b\bigr)
\ar[d,"\varepsilon_\beta"]
\\
g_!\gamma_{(1)}\gamma^*\bigl(c\otimes g^*(b)\bigr)
\ar[r,"g_!\varepsilon_\gamma"']
g_!\bigl(c\otimes g^*(b)\bigr)
\ar[r,"\pf_g"']
g_!(c)\otimes b.
\end{tikzcd}
\]

Here, the lower right square commutes by naturality of $\varepsilon_\beta$, and
the top square commutes by <ref>. The diagrams $(B)$ and $(B')$
commute by the following general fact: Consider the left diagram of functors

\[
\begin{tikzcd}
\cat X
\ar[r,shift left,"L"] \ar[d,"F"']
\ar[dr,Rightarrow,shorten=1em,"\chi" description]
\cat Y
\ar[l,shift left,"R"] \ar[d,"G"]
L'FR \ar[r,"L'\chi"] \ar[d,"l(\chi)R"'] & L'R'G \ar[d,"\varepsilon'G"]
\\
\cat X'
\ar[r,shift left,"L'"]
\cat Y'
\ar[l,shift left,"R'"],
GLR \ar[r,"G\varepsilon"'] & G
\end{tikzcd}
\]

where $\chi\colon FR\To R'G$ is a natural transformation with left mate
$l(\chi)\colon L'F\To GL$. Denote by $\varepsilon\colon LR\To \id_{\cat Y}$ and $\varepsilon'\colon L'R'\To \id_{\cat Y'}$ the counits of the respective adjunctions. Then the right diagram above commutes, since the diagram

\[
\begin{tikzcd}[proof,sep=large]
\ar[d,"L'F\eta R" description] \ar[dr,equals,bend left]
\ar[ddd, start anchor=south west, end anchor=north west,bend right,"l(\chi)R"']
\\
\ar[r,"L'FR\varepsilon"] \ar[d,"L'\chi LR" description]
\ar[d,"L'\chi"]
\\
\ar[d,"\varepsilon'GLR" description] \ar[r,"L'R'G\varepsilon"]
\ar[d,"\varepsilon'G"]
\\
\ar[r,"G\varepsilon"']
\end{tikzcd}
\]

is commutative, where $\eta\colon \id_{\cat X}\To RL$ denotes the unit of the
adjunction $L\dashv R$.

Consider a diagram

\[
\begin{tikzcd}
& & \cat A
\ar[dl,shift right,"f^*"'] \ar[dd,shift left,bend left,"h^*"]
\\
\cat D
\ar[urr,bend left,"\alpha^*"] \ar[r,"\beta^*"] \ar[drr,bend right,"\gamma^*"']
\cat B
\ar[ur,shift right,dashed,"f_!"'] \ar[dr,shift right,"g^*"']
\\
& &
\cat C
\ar[ul,shift right,dashed, "g_!"'] \ar[uu,shift left, dashed, bend right,
\end{tikzcd}
\]

where the solid diagram commutes and consists of (strongly) symmetric monoidal
functors between symmetric monoidal categories, and where the dashed diagram
commutes. The commutativity of the right triangles is witnessed by natural

\[
\lambda\colon h_! \Raiso f_!g_!
\qquad\text{and}\qquad
\mu\colon h^* \Raiso g^*f^*,
\]

where $\mu$ is monoidal. We make the following assumption:

*  The functors $\alpha^*$, $\beta^*$, and $\gamma^*$
admit left adjoints:

\[
\alpha_{(1)}\dashv \alpha^*,\qquad \beta_{(1)}\dashv \beta^*,\qquad
\gamma_{(1)}\dashv \gamma.
\]

Assume moreover that there are natural isomorphisms

\[
\begin{matrix}
\pf_f\colon & f_!\bigl(b\otimes f^*(a)\bigr) &\raiso& f_!(b)\otimes a,\\
\pf_g\colon & g_!\bigl(c\otimes g^*(b)\bigr) &\raiso& g_!(c)\otimes b,\\
\pf_h\colon & h_!\bigl(c\otimes h^*(a)\bigr) &\raiso& h_!(c)\otimes a,
\end{matrix}
\]

which satisfy the following conditions:

*  For all $a\in\cat A$, $c\in \cat C$ the diagram

\[
\begin{tikzcd}
h_!\bigl(c\otimes h^*(a)\bigr)
\ar[rr,"\pf_h"] \ar[d,"\lambda"']
& &
h_!(c)\otimes a
\ar[dd,"\lambda\otimes\id"]
\\
f_!g_!\bigl(c\otimes h^*(a)\bigr)
\ar[d,"f_!g_!(\id\otimes\mu)"']
\\
f_!g_!\bigl(c\otimes g^*f^*(a)\bigr)
\ar[r,"f_!\pf_g"']
f_!\bigl(g_!(c)\otimes f^*(a)\bigr)
\ar[r,"\pf_f"']
f_!g_!(c)\otimes a
\end{tikzcd}
\]

is commutative.

*  For all $a',a\in \cat A$, $b\in \cat B$ the diagram

\[
\begin{tikzcd}
f_!\bigl((b\otimes f^*(a'))\otimes f^*(a)\bigr)
\ar[d,"f_!\assoc"',"\cong"] \ar[r,"\pf_f"]
f_!\bigl(b\otimes f^*(a')\bigr)\otimes a
\ar[r,"\pf_f\otimes\id"]
\bigl(f_!(b)\otimes a'\bigr)\otimes a
\ar[d,"\assoc","\cong"']
\\
f_!\bigl(b\otimes (f^*(a')\otimes f^*(a))\bigr)
\ar[r,"f_!(\id\otimes\mon_f)"']
f_!\bigl(b\otimes f^*(a'\otimes a)\bigr)
\ar[r,"\pf_f"']
f_!(b)\otimes (a'\otimes a)
\end{tikzcd}
\]

is commutative, and similarly with $f$ replaced by $g$. Here, $\assoc$ denotes
the associativity constraint in the respective monoidal categories.

Finally, let $\wt{\pf}_g$ be the unique natural isomorphism making the

\[
\begin{tikzcd}
g_!\bigl(g^*(b)\otimes c\bigr)
\ar[r,"\wt{\pf}_g"] \ar[d,"\sym"',"\cong"]
b\otimes g_!(c)
\ar[d,"\sym","\cong"']
\\
g_!\bigl(c\otimes g^*(b)\bigr)
\ar[r,"\pf_g"']
g_!(c)\otimes b
\end{tikzcd}
\]

commutative, where $\sym$ denotes the symmetry constraints in the respective
symmetric monoidal categories.

For all $b\in \cat B$ and $c',c\in \cat C$ the following diagram commutes:

\[
\begin{tikzcd}[font=\small,labels={font=\tiny},column sep=3em]
\alpha_{(1)}h_!\bigl((g^*(b)\otimes c')\otimes c\bigr)
\ar[d,"\alpha_{(1)}\lambda"']
\ar[r,"\ltm_{\alpha,h}"]
\alpha_{(1)}h_!\bigl(g^*(b)\otimes c'\bigr)\otimes \gamma_{(1)}(c)
\ar[r,"\alpha_{(1)}\lambda \otimes\id"]
\alpha_{(1)}f_!g_!\bigl(g^*(b)\otimes c'\bigr)\otimes \gamma_{(1)}(c)
\ar[d,"\alpha_{(1)}f_!\wt{\pf}_g\otimes\id"]
\\
\alpha_{(1)}f_!g_!\bigl((g^*(b)\otimes c')\otimes c\bigr)
\ar[d,"\alpha_{(1)}f_!g_!\assoc"']
& &
\alpha_{(1)}f_!\bigl(b\otimes g_!(c')\bigr)\otimes \gamma_{(1)}(c)
\ar[d,"\ltm_{\alpha,f}\otimes\id"]
\\
\alpha_{(1)}f_!g_!\bigl(g^*(b)\otimes (c'\otimes c)\bigr)
\ar[d,"\alpha_{(1)}f_!\wt{\pf}_g"']
& &
\bigl(\alpha_{(1)}f_!(b)\otimes \beta_{(1)}g_!(c')\bigr)\otimes \gamma_{(1)}(c)
\ar[d,"\assoc"]
\\
\alpha_{(1)}f_!\bigl(b\otimes g_!(c'\otimes c)\bigr)
\ar[r,"\ltm_{\alpha,f}"']
\alpha_{(1)}f_!(b)\otimes \beta_{(1)}g_!(c'\otimes c)
\ar[r,"\id\otimes\ltm_{\beta,g}"']
\alpha_{(1)}f_!(b)\otimes \bigl(\beta_{(1)}g_!(c')\otimes \gamma_{(1)}(c)\bigr),
\end{tikzcd}
\]

where $\ltm_{\alpha,h}$, $\ltm_{\alpha,f}$, and $\ltm_{\beta,g}$ are defined as
in <ref>.

It suffices to show that the diagram

\[ % {{{
\hspace{-6em}
\begin{tikzcd}[proof]
\alpha_{(1)}h_!\bigl((g^*(b)\otimes c') \otimes h^*\alpha^*(d)\bigr)
\ar[d,"\alpha_{(1)}\lambda(\id\otimes\mu)"']
\ar[rr,"\alpha_{(1)}\pf_h"]
& &
\alpha_{(1)}\bigl(h_!(g^*(b)\otimes c')\otimes \alpha^*(d)\bigr)
\ar[r,"\lpf_\alpha"]
\ar[d,"\alpha_{(1)}(\lambda\otimes\id)"]
\alpha_{(1)}h_!\bigl(g^*(b)\otimes c')\otimes d
\ar[d,"\alpha_{(1)}\lambda\otimes \id"]
\\
\alpha_{(1)}f_!g_!\bigl((g^*(b)\otimes c')\otimes g^*f^*\alpha^*(d)\bigr)
\ar[d,"\alpha_{(1)}f_!g_!\assoc"']
\ar[r,"\alpha_{(1)}f_!\pf_g"]
\ar[ddr,phantom,"\ref{lwirth-trans-I}"]
\alpha_{(1)}f_!\bigl(g_!(g^*(b)\otimes c')\otimes f^*\alpha^*(d)\bigr)
\ar[d,"\alpha_{(1)}f_!(\wt{\pf}_g\otimes\id)"]
\ar[r,"\alpha_{(1)}\pf_f"]
\alpha_{(1)}\bigl(f_!g_!(g^*(b)\otimes c')\otimes \alpha^*(d)\bigr)
\ar[r,"\lpf_\alpha"]
\ar[dd,"\alpha_{(1)}(f_!\wt{\pf}_g\otimes\id)"]
\alpha_{(1)}f_!g_!\bigl(g^*(b)\otimes c'\bigr)\otimes d
\ar[dd,"\alpha_{(1)}f_!\wt{\pf}_g\otimes \id"]
\\
\alpha_{(1)}f_!g_!\bigl(g^*(b)\otimes (c'\otimes g^*\beta^*(d))\bigr)
\ar[d,"\alpha_{(1)}f_!\wt{\pf}_g"']
\alpha_{(1)}f_!\bigl((b\otimes g_!(c'))\otimes \beta^*(d)\bigr)
\ar[d,"\alpha_{(1)}f_!\assoc"']
\ar[dr,"\alpha_{(1)}\pf_f"]
\\
\alpha_{(1)}f_!\bigl(b\otimes g_!(c'\otimes g^*\beta^*(d))\bigr)
\ar[d,"\ltm_{\alpha,f}"']
\ar[r,"\alpha_{(1)}f_!(\id\otimes \pf_g)"]
\alpha_{(1)}f_!\bigl(b\otimes (g_!(c')\otimes \beta^*(d))\bigr)
\ar[d,"\ltm_{\alpha,f}"']
\alpha_{(1)}\bigl(f_!(b\otimes g_!(c'))\otimes \alpha^*(d)\bigr)
\ar[r,"\lpf_\alpha"]
\ar[d,phantom, "\ref{lwirth-trans-II}"]
\alpha_{(1)}f_!\bigl(b\otimes g_!(c')\bigr)\otimes d
\ar[d,"\ltm_{\alpha,f}\otimes\id"]
\\
\alpha_{(1)}f_!(b)\otimes \beta_{(1)}g_!\bigl(c'\otimes g^*\beta^*(d)\bigr)
\ar[r,"\id\otimes\beta_{(1)}\pf_g"']
\alpha_{(1)}f_!(b)\otimes \beta_{(1)}\bigl(g_!(c')\otimes \beta^*(d)\bigr)
\ar[r,"\id\otimes\lpf_\beta"']
\alpha_{(1)}f_!(b)\otimes \bigl(\beta_{(1)}g_!(c')\otimes d\bigr)
\bigl(\alpha_{(1)}f_!(b)\otimes \beta_{(1)}g_!(c')\bigr)\otimes d
\ar[l,"\assoc"]
\end{tikzcd}
\]

commutes, because then passing to the left mates at $\lpf_\alpha
\circ\alpha_{(1)}\pf_h \colon \alpha_{(1)}h_!\bigl((g^*(b)\otimes c')\otimes
\blank) h^*\alpha^* \To \alpha_{(1)}h_!\bigl(g^*(b)\otimes c'\bigr)\otimes
\blank$ shows that the diagram in the lemma commutes. The upper left rectangle
commutes by <ref>, and the
commutativity of all squares except <ref> and
<ref> is clear.

*  We need to show that the outer diagram

\[ % {{{
\begin{tikzcd}[proof]
g_!\bigl((g^*(b)\otimes c')\otimes g^*(b')\bigr)
\ar[d,"g_!(s\otimes\id)"']
\ar[r,"\pf_g"]
\ar[ddddd,start anchor=south west, end anchor=north west,bend
g_!\bigl(g^*(b)\otimes c'\bigr)\otimes b'
\ar[d,"g_!s\otimes \id"]
\ar[r,"\wt{\pf}_g\otimes\id"]
\bigl(b\otimes g_!(c')\bigr)\otimes b'
\ar[d,"s\otimes \id"]
\ar[ddddd,start anchor=south east, end anchor=north east, bend left, "\assoc"]
\\
g_!\bigl((c'\otimes g^*(b)\bigr)\otimes g^*(b')\bigr)
\ar[d,"g_!\assoc"']
\ar[r,"\pf_g"]
g_!\bigl(c'\otimes g^*(b)\bigr)\otimes b'
\ar[r,"\pf_g\otimes\id"]
\ar[d,phantom,"(*)"{font=\tiny}]
\bigl(g_!(c')\otimes b\bigr)\otimes b'
\ar[d,"\assoc"]
\\
g_!\bigl(c'\otimes (g^*(b)\otimes g^*(b'))\bigr)
\ar[d,"g_!(\id\otimes s)"']
\ar[r,"g_!(\id\otimes\mon_g)"]
g_!\bigl(c'\otimes g^*(b\otimes b')\bigr)
\ar[d,"g_!(\id\otimes g^*s)"]
\ar[r,"\pf_g"]
g_!(c')\otimes (b\otimes b')
\ar[d,"\id\otimes s"]
\\
g_!\bigl(c'\otimes (g^*(b')\otimes g^*(b))\bigr)
\ar[r,"g_!(\id\otimes\mon_g)"]
g_!\bigl(c'\otimes g^*(b'\otimes b)\bigr)
\ar[r,"\pf_g"']
\ar[d,phantom,"(**)"{font=\tiny}]
g_!(c')\otimes (b'\otimes b)
\\
g_!\bigl((c'\otimes g^*(b'))\otimes g^*(b)\bigr)
\ar[u,"g_!\assoc"]
\ar[r,"\pf_g"]
g_!\bigl(c'\otimes g^*(b')\bigr)\otimes b
\ar[r,"\pf_g\otimes\id"]
\bigl(g_!(c')\otimes b'\bigr)\otimes b
\ar[u,"\assoc"']
\\
g_!\bigl(g^*(b)\otimes (c'\otimes g^*(b'))\bigr)
\ar[u,"g_!s"]
\ar[r,"\pf_g"']
b\otimes g_!\bigl(c'\otimes g^*(b')\bigr)
\ar[u,"s"]
\ar[r,"\id\otimes\pf_g"']
b\otimes \bigl(g_!(c')\otimes b'\bigr)
\ar[u,"s"']
\end{tikzcd}
\]

commutes, where we have put $b'\coloneqq f^*\alpha^*(d)$. It is clear that all
the small squares commute; for example, the left square in
the middle commutes, because $g$ is a symmetric monoidal functor. The diagrams
marked $(*)$ and
$(**)$ commute by <ref>. The diagrams on the far left and far right
commute by the hexagon identity.

*  After passing to the right mate at
$\id\otimes\lpf_\beta$ or $\ltm_{\alpha,f}\otimes \id$, and using $\beta^* =
f^*\alpha^*$, it suffices to show that the following diagram commutes:

\[
\begin{tikzcd}[proof]
\alpha_{(1)}f_!\bigl(b\otimes (f^*\alpha^*(d')\otimes f^*\alpha^*(d))\bigr)
\ar[r,"\alpha_{(1)}f_!(\id\otimes \mon_f)"]
\alpha_{(1)}f_!\bigl(b\otimes f^*(\alpha^*(d')\otimes \alpha^*(d))\bigr)
\ar[r,"\alpha_{(1)}f_!(\id\otimes f^*\mon_\alpha)"]
\ar[d,"\alpha_{(1)}\pf_f"]
\alpha_{(1)}f_!\bigl(b\otimes f^*\alpha^*(d'\otimes d)\bigr)
\ar[d,"\alpha_{(1)}\pf_f"]
\\
\alpha_{(1)}f_!\bigl((b\otimes f^*\alpha^*(d'))\otimes f^*\alpha^*(d)\bigr)
\ar[u,"\alpha_{(1)}f_!\assoc"]
\ar[d,"\alpha_{(1)}\pf_f"']
\alpha_{(1)}\bigl(f_!(b)\otimes (\alpha^*(d')\otimes \alpha^*(d))\bigr)
\ar[r,"\alpha_{(1)}(\id\otimes\mon_\alpha)"]
\alpha_{(1)}\bigl(f_!(b)\otimes \alpha^*(d'\otimes d)\bigr)
\ar[d,"\lpf_\alpha"]
\\
\alpha_{(1)}\bigl(f_!(b\otimes f^*\alpha^*(d'))\otimes \alpha^*(d)\bigr)
\ar[d,"\lpf_\alpha"']
\ar[r,"\alpha_{(1)}(\pf_f\otimes\id)"]
\alpha_{(1)}\bigl((f_!(b)\otimes \alpha^*(d'))\otimes \alpha^*(d)\bigr)
\ar[u,"\alpha_{(1)}\assoc"]
\ar[d,"\lpf_\alpha"']
\alpha_{(1)}f_!(b)\otimes (d'\otimes d)
\\
\alpha_{(1)}f_!\bigl(b\otimes f^*\alpha^*(d')\bigr)\otimes d
\ar[r,"\alpha_{(1)}\pf_f\otimes\id"']
\alpha_{(1)}\bigl(f_!(b)\otimes \alpha^*(d')\bigr) \otimes d
\ar[r,"\lpf_\alpha\otimes\id"']
\bigl(\alpha_{(1)}f_!(b)\otimes d'\bigr)\otimes d
\ar[u,"\assoc"']
\end{tikzcd}
\]

The lower left square commutes by naturality of $\lpf_\alpha$, and the upper
right square by the naturality of $\alpha_{(1)}\pf_f$. The upper left rectangle
commutes by <ref>. For the lower right rectangle, we pass to the
right mate at, say, $\lpf_\alpha\colon \alpha_{(1)}(-\otimes\alpha^*(d'\otimes
d)) \Rightarrow (-\otimes (d'\otimes d))\alpha_{(1)}$, and then it suffices to
show that the diagram

\[
\begin{tikzcd}[proof]
\bigl(\alpha^*(d'')\otimes \alpha^*(d')\bigr)\otimes \alpha^*(d)
\ar[r,"\mon_\alpha\otimes\id"]
\ar[d,"\assoc"']
\alpha^*(d''\otimes d')\otimes \alpha^*(d)
\ar[r,"\mon_\alpha"]
\alpha^*\bigl((d''\otimes d')\otimes d\bigr)
\ar[d,"\alpha^*\assoc"]
\\
\alpha^*(d'')\otimes \bigl(\alpha^*(d')\otimes \alpha^*(d)\bigr)
\ar[r,"\id\otimes\mon_\alpha"']
\alpha^*(d'')\otimes \alpha^*(d'\otimes d)
\ar[r,"\mon_\alpha"']
\alpha^*\bigl(d''\otimes (d'\otimes d)\bigr).
\end{tikzcd}
\]

is commutative. But this follows from the fact that $\alpha$ is a monoidal
functor. Thus, we deduce that <ref> commutes.