∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D}
  (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D)
  (g :
    { g //
      CategoryTheory.CategoryStruct.comp (G.map (F.map g)) (G.map (adj.counit.app B)) =
        CategoryTheory.CategoryStruct.comp A.a g }),
  CategoryTheory.CategoryStruct.comp (G.map (F.map ↑g)) (G.map (adj.counit.app B)) =
    CategoryTheory.CategoryStruct.comp A.a ↑g