关于Hom集自然变换相关引理的名称、参考文献及与Yoneda引理关系的技术问询

Question 1: 有没有人知道下面这个引理的名称，或者相关参考文献？

Lemma: 给定函子 $G_1,G_2: \mathscr{C} \to \mathscr{G}$，且存在自然变换 $G_1 \implies G_2$；同时给定函子 $F_1, F_2: \mathscr{C} \to \mathscr{F}$，且存在自然变换 $\operatorname{Hom}{\mathscr{G}} \circ (G_1^{\operatorname{op}}, G_2) \implies \operatorname{Hom}{\mathscr{F}} \circ (F_1^{\operatorname{op}}, F_2)$，那么存在自然变换 $F_1 \implies F_2$。

（符号定义：$\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}}$）

Question 2: 如果上述引理可以用来证明Yoneda引理，具体该怎么操作？如果这个引理是Yoneda引理的推论，那推导过程又是怎样的？

可选背景说明：我会在下面的回答里附上这个引理的证明。
我是在尝试证明伴随函子定义中Hom集的自然双射能推导出单位和余单位自然变换时发现这个引理的。当时我有点困惑，因为证明过程用到的假设条件很少，最后我把证明提炼成了上面这个引理。

从表面上看，这个引理应该和Yoneda引理有关联：两个引理都涉及到包含Hom函子的自然变换，而且都可以用来证明伴随函子中的单位和余单位自然变换的存在性。另外，两者的证明似乎都涉及到“自然变换由另一个自然变换的分量决定”这一点（毕竟恒等态射是恒等自然变换的分量）。

如果这个引理真的能用来证明Yoneda引理，那有两个点让我不解：

• 这个引理为什么没有名字/没有被更广泛地认知；
• 我还没搞清楚怎么用它来证明Yoneda引理。

备注：内容来源于stack exchange，提问作者hasManyStupidQuestions