-- 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
x_1 : Cᵒᵖ
x : (↑(obj (obj preadditiveYoneda (G.obj X)) x_1) : Type v₁)
⊢ Eq (α :=
    (↑(((preadditiveYoneda ⋙
                  obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                    obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
              Y).obj
          x_1) :
      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_1) :
          (a :
              (↑(((G ⋙
                            preadditiveYoneda ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        X).obj
                    x_1) :
                Type (max v₁ v₂))) →
            (↑(((preadditiveYoneda ⋙
                          (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                            (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  x_1) :
              Type (max v₁ v₂)))
        { down := x } :
      (↑(((preadditiveYoneda ⋙
                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                Y).obj
            x_1) :
        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_1) :
          (a :
              (↑(((G ⋙
                            preadditiveYoneda ⋙
                              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                        X).obj
                    x_1) :
                Type (max v₁ v₂))) →
            (↑(((preadditiveYoneda ⋙
                          (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                            (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
                      Y).obj
                  x_1) :
              Type (max v₁ v₂)))
        { down := x } :
      (↑(((preadditiveYoneda ⋙
                    obj (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat) F.op ⋙
                      obj (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat) AddCommGrpCat.uliftFunctor).obj
                Y).obj
            x_1) :
        Type (max v₁ v₂)))

Tactic:
AddEquiv.ulift.injective ((adj.homEquiv_naturality_right_symm x f))

Premises used: AddEquiv.ulift, AddEquiv.injective, CategoryTheory.Adjunction.homEquiv_naturality_right_symm