Question 1: Does anyone know a name, or have a reference, for the following lemma?
$\newcommand{\Hom}{\operatorname{Hom}}$$\newcommand{\F}{\mathscr{F}}$$\newcommand{\G}{\mathscr{G}}$$\newcommand{\op}{\operatorname{op}}$$\newcommand{\C}{\mathscr{C}}$ $\newcommand{\Id}{\operatorname{Id}}$$\newcommand{\Ob}{\operatorname{Ob}}$$\newcommand{\Set}{\operatorname{Set}}$$\newcommand{\eval}{\operatorname{eval}}$Lemma: Given functors $G_1,G_2: \C \to \G$ such that there exists a natural transformation $G_1 \implies G_2$, and functors $F_1, F_2: \C \to \F$ such that there exists a natural transformation ${ \Hom_{\G} \circ (G_1^{\op}, G_2) \implies \Hom_{\F} \circ (F_1^{\op}, F_2) }$, then there exists a natural transformation $F_1 \implies F_2$.
Question 2: If the above lemma can be used to prove the Yoneda lemma, how would one do so? If the above lemma is a corollary of the Yoneda lemma, then how?
Optional context: I will put a proof of this lemma in an answer below.
I found the lemma when trying to prove that the natural bijection of Hom sets in the definition of an adjunction implies the existence of unit and counit natural transformations. I was confused because the proof seemed to use very little of the assumptions available, and what I was able to distill the proof to was the above lemma.
Superficially, it seems like this lemma should be related to the Yoneda lemma. Both lemmas involve natural transformations where at least one of the functors is a Hom functor, and both can be used to prove the existence of the unit and counit natural transformations in an adjunction. They also both seem to have proofs involving natural transformations being determined by the components of another natural transformation (given that identity morphisms are the components of identity natural transformations).
If this lemma can be used to prove Yoneda, (1) it seems odd that this lemma doesn't have a name / isn't more widely known, and (2) I haven't been able to figure out how to use it to prove Yoneda.
Proof: For every $c \in \Ob(\C)$, let $\lambda_c$ denote the corresponding component of the natural transformation $G_1 \implies G_2$.
For every ${(c_1, c_2) \in \Ob(\C^{\op} \times \C)}$, let $\eta_{c_1, c_2}$ denote the corresponding component of the natural transformation ${ \Hom_{\G} \circ (G_1^{\op}, G_2) \implies \Hom_{\F} \circ (F_1^{\op}, F_2) }$.
Then the claim is that the $\eta_{c,c}(\lambda_c) =: \mu_c$ for every $c \in \Ob(\C)$ define the components of a natural transformation $F_1 \implies F_2$. What we need to show to prove the claim is that for every $c_1 \overset{h}{\longrightarrow} c_2$ in $\operatorname{Mor}(\C)$ the square:
$$ \require{AMScd} \begin{CD} F_1(c_1) @>> F_1(h) > F_1(c_2) \\ @VV \displaystyle \mu_{c_1} V @VV \displaystyle \mu_{c_2} V \\ F_2(c_1) @>> F_2(h) > F_2(c_2) \end{CD} $$
commutes, i.e. that $\eta_{c_2, c_2}(\lambda_{c_2}) \circ F_1(h) = \mu_{c_2} \circ F_1(h) = F_2(h) \circ \mu_{c_1} = F_2(h) \circ \eta_{c_1, c_1} (\lambda_{c_1})$.
To show this, we look at two naturality squares for $\Hom_{\G} \circ (G_1^{\op}, G_2) \implies \Hom_{\F} \circ (F_1^{\op}, F_2)$:
$$ \require{AMScd} \begin{CD} \Hom_{\G}(G_1(c_1), G_2(c_1)) @> \displaystyle (\Hom_{\G} \circ (G_1^{\op}, G_2))(h_1) > \alpha_1 \mapsto G_2(\pi_2(h_1)) \circ \alpha_1 \circ G_1(\pi_1(h_1)) > \Hom_{\G}(G_1(c_1), G_2(c_2)) @< \displaystyle (\Hom_{\G} \circ (G_1^{\op}, G_2))(h_2) < \alpha_2 \mapsto G_2(\pi_2(h_2)) \circ \alpha_2 \circ G_1(\pi_1(h_2)) < \Hom_{\G}(G_1(c_2), G_2(c_2)) \\ @VV \displaystyle \eta_{c_1, c_1} V @VV \displaystyle \eta_{c_1, c_2} V @VV \displaystyle \eta_{c_2, c_2} V \\ \Hom_{\F}(F_1(c_1), F_2(c_1)) @> \beta_1 \mapsto F_2(\pi_2(h_1)) \circ \beta_1 \circ F_1(\pi_1(h_1)) > \displaystyle (\Hom_{\F} \circ (F_1^{\op}, F_2))(h_1) > \Hom_{\F}(F_1(c_1), F_2(c_2)) @< \beta_2 \mapsto F_2(\pi_2(h_2)) \circ \beta_2 \circ F_1(\pi_1(h_2)) < \displaystyle (\Hom_{\F} \circ (F_1^{\op}, F_2))(h_2) < \Hom_{\F} (F_1(c_2), F_2(c_2)) \end{CD} $$
The crux then comes down to making clever choices for the morphisms ${(c_1, c_1) \overset{h_1}{\longrightarrow} (c_1, c_2)}$ and ${(c_2, c_2) \overset{h_2}{\longrightarrow} (c_1, c_2)}$ in ${\C^{\op} \times \C }$. What works is $h_1 := {(c_1 \overset{\Id_{c_1}}{\longleftarrow} c_1, c_1 \overset{h}{\longrightarrow} c_2 )}$ and $h_2 := {(c_2 \overset{h}{\longleftarrow} c_1, c_2 \overset{\Id_{c_2}}{\longrightarrow} c_2)}$.
Choosing $\lambda_{c_1} \in \Hom_{\G}(G_1(c_1), G_2(c_1))$ and chasing it around the left naturality square leads to $$\eta_{c_1, c_2} (G_2(h) \circ \lambda_{c_1}) = F_2(h) \circ \mu_{c_1}. $$ Choosing $\lambda_{c_2} \in \Hom_{\G}(G_1(c_2), G_2(c_2))$ and chasing it around the right naturality square leads to $$\eta_{c_1, c_2}(\lambda_{c_2} \circ G_1(h)) = \mu_{c_2} \circ F_1(h).$$
Now it may initially seem that all hope is lost because $\eta_{c_1, c_2} (G_2(h) \circ \lambda_{c_1})$ is not obviously equal to $\eta_{c_1, c_2}(\lambda_{c_2} \circ G_1(h))$. However, the $\lambda_c$'s are themselves components of the natural transformation $G_1 \implies G_2$, which associates the morphism $c_1 \overset{h}{\longrightarrow} c_2$ in $\C$ with the naturality square: $$ \require{AMScd} \begin{CD} G_1(c_1) @> G_1(h) >> G_1(c_2) \\ @V \displaystyle \lambda_{c_1} VV @VV \displaystyle \lambda_{c_2} V \\ G_2(c_1) @> G_2(h) >> G_2(c_2) \end{CD} $$ in $\G$. In other words, it is a direct consequence of naturality of $\lambda$ that $G_2(h) \circ \lambda_{c_1} = \lambda_{c_2} \circ G_1(h) =: \tilde{h}$. Hence $$ F_2(h) \circ \mu_{c_1} = \eta_{c_1, c_2} (G_2(h) \circ \lambda_{c_1}) = \eta_{c_1, c_2}(\tilde{h}) = \eta_{c_1, c_2}(\lambda_{c_2} \circ G_1(h)) = \mu_{c_2} \circ F_1(h), $$ with the equality of the first and last term being exactly what was needed to be shown for the $\mu_c$'s to be the components of a natural transformation $F_1 \implies F_2$. $\square$
Proof of existence of unit and counit natural transformations: Let's say we have an adjunction between functors $\newcommand{\B}{\mathscr{B}}\newcommand{\E}{\mathscr{E}}\newcommand{\Set}{\operatorname{Set}}$ $I: \B \to \E$ and $T: \E \to \B$, so a natural isomorphism between the functors $\Hom_{\B} \circ ( (\Id_{\B})^{\op}, T) : \B^{\op} \times \E \to \Set$ and $\Hom_{\E} \circ (I^{\op}, \Id_{\E}): \B^{\op} \times \E \to \Set$.
Via "pre-whiskering" the natural transformation $\Hom_{\E} \circ (I^{\op}, \Id_{\E}) \implies \Hom_{\B} \circ ( (\Id_{\B})^{\op}, T)$ with the functor $((\Id_{\B})^{\op}, I): \B^{\op} \times \B \to \B^{\op} \times \E$, we get a natural transformation $$ \Hom_{\E} \circ (I^{\op}, I) \implies \Hom_{\B} \circ ( (\Id_{\B})^{\op}, T \circ I)$$ of functors $\B^{\op} \times \B \to \Set$. Then the identity natural transformation $\Id_I: I \times I$ combined with the above lemma gives us a natural transformation $\Id_{\B} \implies T \circ I$.
Similarly, via "pre-whiskering" the natural transformation $\Hom_{\B} \circ ( (\Id_{\B})^{\op}, T) \implies \Hom_{\E} \circ (I^{\op}, \Id_{\E})$ with the functor $(T^{\op}, \Id_{\E}): \E^{\op} \times \E \to \B^{\op} \times \E$, we get a natural transformation $$ \Hom_{\B} \circ ( T^{\op}, T) \implies \Hom_{\E} \circ (I^{\op} \circ T^{\op}, \Id_{\E})$$ of functors $\E^{\op} \times \E \to \Set$. Then the identity natural transformation $\Id_T: T \implies T$ combined with the above lemma gives us a natural transformation $I \circ T \implies \Id_{\E}$.
Attempt for question 2:$\newcommand{\eval}{\operatorname{eval}}$ Because this lemma seems simpler and more general than the Yoneda lemma (no restrictions on the categories $\C$, $\F$, or $\G$, only a one-directional natural transformation, not a natural isomorphism), it seems like if there is a relationship to the Yoneda lemma, that the Yoneda lemma would either be a consequence of or a special case of this lemma.
For Yoneda, we are trying to prove a natural isomorphism between two functors ${\C \times [\C, \Set] \to \Set}$, namely $F_1 = \Hom_{[\C, \Set]} \circ ( (\Hom_{\C}(\bullet, -))^{\op}, \Id_{[\C, \Set]})$ (where I have used the non-standard notation $X(\bullet, -)$ to denote currying in the first coordinate) to $F_2 = \eval_{[\C, \Set]}$.
So if Yoneda is a corollary of the above lemma, then we need to find some category $\G$, and two functors $G_1, G_2:\C \times [\C, \Set] \to \G$ such that $G_1$ and $G_2$ are naturally isomorphic and such that there are natural transformations $$\Hom_{\G} \circ (G_1^{\op}, G_2) \implies \Hom_{\Set} ( (Hom_{[\C, \Set]} \circ ( (\Hom_{\C}(\bullet, -))^{\op}, \Id_{[\C, \Set]}))^{\op}, \eval_{[\C, \Set]}) $$ and $$ \Hom_{\G} \circ (G_2^{\op}, G_1) \implies \Hom_{\Set} ( (\eval_{[\C, \Set]})^{\op} , Hom_{[\C, \Set]} \circ ( (\Hom_{\C}(\bullet, -))^{\op}, \Id_{[\C, \Set]}) ) .$$ Even acknowledging that I am getting confused by the complicated "type signatures", I don't see any obvious candidates for $G_1, G_2$, and $\G$.
Possibly related questions:
Are fully faithful functors left-cancellable up to natural isomorphism?
Natural Transformation Between Covariant Hom-Functors
Adjoint Functors induce Natural Transformations
Natural transformation induced by adjoint functors.
Proving that the transformation obtained from an adjoint pair is natural
The Natural Isomorphism in Yoneda Lemma
Yoneda Lemma and isomorphisms
bivariate Yoneda lemma
Is the natural isomorphism in an adjunction uniquely determined by the pair of adjoint functors