-- 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
X Y : D
f : X ⟶ Y
w :
  ∀ (x : Cᵒᵖ) (x_1 : (↑(obj (obj preadditiveYoneda (G.obj X)) x) : Type v₁)),
    Eq (α :=
      (↑(((preadditiveYoneda ⋙
                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                Y).obj
            x) :
        Type (max v₁ v₂)))
      ((AddCommGrpCat.Hom.hom
              (NatTrans.app
                ((G ⋙
                        preadditiveYoneda ⋙
                          obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).map
                    f ≫
                  Iso.hom
                    ((fun (Y : D) ↦
                        (NatIso.ofComponents
                            (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 ≅
                            (preadditiveYoneda ⋙
                                  obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                                    obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat)
                                      AddCommGrpCat.uliftFunctor).obj
                              Y))
                      Y))
                x) :
            (a :
                (↑(((G ⋙
                              preadditiveYoneda ⋙
                                (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                          X).obj
                      x) :
                  Type (max v₁ v₂))) →
              (↑(((preadditiveYoneda ⋙
                            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        Y).obj
                    x) :
                Type (max v₁ v₂)))
          { down := x_1 } :
        (↑(((preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              x) :
          Type (max v₁ v₂)))
      ((AddCommGrpCat.Hom.hom
              (NatTrans.app
                (Iso.hom
                    ((fun (Y : D) ↦
                        (NatIso.ofComponents
                            (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 ≅
                            (preadditiveYoneda ⋙
                                  obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                                    obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat)
                                      AddCommGrpCat.uliftFunctor).obj
                              Y))
                      X) ≫
                  (preadditiveYoneda ⋙
                        obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                          obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).map
                    f)
                x) :
            (a :
                (↑(((G ⋙
                              preadditiveYoneda ⋙
                                (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                          X).obj
                      x) :
                  Type (max v₁ v₂))) →
              (↑(((preadditiveYoneda ⋙
                            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        Y).obj
                    x) :
                Type (max v₁ v₂)))
          { down := x_1 } :
        (↑(((preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y).obj
              x) :
          Type (max v₁ v₂)))
⊢ (G ⋙ preadditiveYoneda ⋙ obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).map f ≫
      Iso.hom
        ((fun (Y : D) ↦
            (NatIso.ofComponents
                (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 ≅
                (preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y))
          Y) =
    Iso.hom
        ((fun (Y : D) ↦
            (NatIso.ofComponents
                (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 ≅
                (preadditiveYoneda ⋙
                      obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                        obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                  Y))
          X) ≫
      (preadditiveYoneda ⋙
            obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
              obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).map
        f

Tactic:
ext _ ⟨x⟩