-- Module: Mathlib.CategoryTheory.Adjunction.Additive
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.Additive
Y : D
X Y_1 : Cᵒᵖ
g : X ⟶ Y_1
hf :
  ∀ (y : (↑(obj (obj preadditiveYoneda (G.obj Y)) X) : Type v₁)),
    Eq (α :=
      (↑(((preadditiveYoneda ⋙
                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                Y).obj
            Y_1) :
        Type (max v₁ v₂)))
      ((AddCommGrpCat.Hom.hom
              (((G ⋙
                          preadditiveYoneda ⋙
                            obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                      Y).map
                  g ≫
                Iso.hom
                  ((fun (X : Cᵒᵖ) ↦
                      (AddEquiv.toAddCommGrpIso
                          (AddEquiv.trans AddEquiv.ulift
                            (AddEquiv.trans (AddEquiv.symm (adj.homAddEquiv (unop X) Y))
                              (AddEquiv.symm AddEquiv.ulift))) :
                        ((G ⋙
                                    preadditiveYoneda ⋙
                                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat)
                                        AddCommGrpCat.uliftFunctor).obj
                                Y).obj
                            X ≅
                          ((preadditiveYoneda ⋙
                                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat)
                                        AddCommGrpCat.uliftFunctor).obj
                                Y).obj
                            X))
                    Y_1)) :
            (a :
                (↑(((G ⋙
                              preadditiveYoneda ⋙
                                (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                          Y).obj
                      X) :
                  Type (max v₁ v₂))) →
              (↑(((preadditiveYoneda ⋙
                            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        Y).obj
                    Y_1) :
                Type (max v₁ v₂)))
          { down := y } :
        (↑(((preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              Y_1) :
          Type (max v₁ v₂)))
      ((AddCommGrpCat.Hom.hom
              (Iso.hom
                  ((fun (X : Cᵒᵖ) ↦
                      (AddEquiv.toAddCommGrpIso
                          (AddEquiv.trans AddEquiv.ulift
                            (AddEquiv.trans (AddEquiv.symm (adj.homAddEquiv (unop X) Y))
                              (AddEquiv.symm AddEquiv.ulift))) :
                        ((G ⋙
                                    preadditiveYoneda ⋙
                                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat)
                                        AddCommGrpCat.uliftFunctor).obj
                                Y).obj
                            X ≅
                          ((preadditiveYoneda ⋙
                                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat)
                                        AddCommGrpCat.uliftFunctor).obj
                                Y).obj
                            X))
                    X) ≫
                ((preadditiveYoneda ⋙
                          obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                            obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                      Y).map
                  g) :
            (a :
                (↑(((G ⋙
                              preadditiveYoneda ⋙
                                (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                          Y).obj
                      X) :
                  Type (max v₁ v₂))) →
              (↑(((preadditiveYoneda ⋙
                            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        Y).obj
                    Y_1) :
                Type (max v₁ v₂)))
          { down := y } :
        (↑(((preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              Y_1) :
          Type (max v₁ v₂)))
⊢ ((G ⋙ preadditiveYoneda ⋙ obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj Y).map
        g ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (AddEquiv.toAddCommGrpIso
                (AddEquiv.trans AddEquiv.ulift
                  (AddEquiv.trans (AddEquiv.symm (adj.homAddEquiv (unop X) Y)) (AddEquiv.symm AddEquiv.ulift))) :
              ((G ⋙
                          preadditiveYoneda ⋙
                            obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  X ≅
                ((preadditiveYoneda ⋙
                          obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                            obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  X))
          Y_1) =
    Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (AddEquiv.toAddCommGrpIso
                (AddEquiv.trans AddEquiv.ulift
                  (AddEquiv.trans (AddEquiv.symm (adj.homAddEquiv (unop X) Y)) (AddEquiv.symm AddEquiv.ulift))) :
              ((G ⋙
                          preadditiveYoneda ⋙
                            obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  X ≅
                ((preadditiveYoneda ⋙
                          obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                            obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  X))
          X) ≫
      ((preadditiveYoneda ⋙
                obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                  obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
            Y).map
        g

Tactic:
ext ⟨y⟩