-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
B : C
n a a' : ℤ
h : n + a = a'
X Y : Cᵒᵖ
f : X ⟶ Y
hf :
  ∀
    (x :
      (↑(Functor.obj
            (shiftFunctor Cᵒᵖ n ⋙ Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
            X) :
        Type v_1)),
    Eq (α :=
      (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) Y) :
        Type v_1))
      ((AddCommGrpCat.Hom.hom
              (Functor.map
                  (shiftFunctor Cᵒᵖ n ⋙
                    Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                  f ≫
                Iso.hom
                  ((fun (A : Cᵒᵖ) ↦
                      (AddEquiv.toAddCommGrpIso
                          (let __Equiv :
                            (↑(Functor.obj
                                    (shiftFunctor Cᵒᵖ n ⋙
                                      Functor.obj preadditiveYoneda
                                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                                    A) :
                                Type v_1) ≃
                              (↑(Functor.obj
                                    (Functor.obj preadditiveYoneda
                                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B))
                                    A) :
                                Type v_1) :=
                            Equiv.trans Quiver.Hom.opEquiv (Equiv.symm (ShiftedHom.opEquiv' n a a' h));
                          { toEquiv := __Equiv, map_add' := ⋯ }) :
                        Functor.obj
                            (shiftFunctor Cᵒᵖ n ⋙
                              Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                            A ≅
                          Functor.obj
                            (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) A))
                    Y)) :
            (a : (↑((shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj X) : Type v_1)) →
              (↑((preadditiveYoneda.obj ((shiftFunctor C a').obj B)).obj Y) : Type v_1))
          x :
        (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) Y) :
          Type v_1))
      ((AddCommGrpCat.Hom.hom
              (Iso.hom
                  ((fun (A : Cᵒᵖ) ↦
                      (AddEquiv.toAddCommGrpIso
                          (let __Equiv :
                            (↑(Functor.obj
                                    (shiftFunctor Cᵒᵖ n ⋙
                                      Functor.obj preadditiveYoneda
                                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                                    A) :
                                Type v_1) ≃
                              (↑(Functor.obj
                                    (Functor.obj preadditiveYoneda
                                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B))
                                    A) :
                                Type v_1) :=
                            Equiv.trans Quiver.Hom.opEquiv (Equiv.symm (ShiftedHom.opEquiv' n a a' h));
                          { toEquiv := __Equiv, map_add' := ⋯ }) :
                        Functor.obj
                            (shiftFunctor Cᵒᵖ n ⋙
                              Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                            A ≅
                          Functor.obj
                            (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) A))
                    X) ≫
                Functor.map (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B))
                  f) :
            (a : (↑((shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj X) : Type v_1)) →
              (↑((preadditiveYoneda.obj ((shiftFunctor C a').obj B)).obj Y) : Type v_1))
          x :
        (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) Y) :
          Type v_1))
⊢ Eq (α :=
    Functor.obj
        (shiftFunctor Cᵒᵖ n ⋙ Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) X ⟶
      Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) Y)
    (Functor.map
        (shiftFunctor Cᵒᵖ n ⋙ Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) f ≫
      Iso.hom
        ((fun (A : Cᵒᵖ) ↦
            (AddEquiv.toAddCommGrpIso
                (let __Equiv :
                  (↑(Functor.obj
                          (shiftFunctor Cᵒᵖ n ⋙
                            Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                          A) :
                      Type v_1) ≃
                    (↑(Functor.obj
                          (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) A) :
                      Type v_1) :=
                  Equiv.trans Quiver.Hom.opEquiv (Equiv.symm (ShiftedHom.opEquiv' n a a' h));
                { toEquiv := __Equiv, map_add' := ⋯ }) :
              Functor.obj
                  (shiftFunctor Cᵒᵖ n ⋙
                    Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                  A ≅
                Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) A))
          Y))
    (Iso.hom
        ((fun (A : Cᵒᵖ) ↦
            (AddEquiv.toAddCommGrpIso
                (let __Equiv :
                  (↑(Functor.obj
                          (shiftFunctor Cᵒᵖ n ⋙
                            Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                          A) :
                      Type v_1) ≃
                    (↑(Functor.obj
                          (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) A) :
                      Type v_1) :=
                  Equiv.trans Quiver.Hom.opEquiv (Equiv.symm (ShiftedHom.opEquiv' n a a' h));
                { toEquiv := __Equiv, map_add' := ⋯ }) :
              Functor.obj
                  (shiftFunctor Cᵒᵖ n ⋙
                    Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
                  A ≅
                Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) A))
          X) ≫
      Functor.map (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') B)) f)

Tactic:
ext