-- 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 m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x_1 : Cᵒᵖ
x :
  (↑(Functor.obj
        (shiftFunctor Cᵒᵖ (m + n) ⋙
          Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B))
        x_1) :
    Type v_1)
⊢ Eq (α :=
    (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') B)) x_1) :
      Type v_1))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (A : Cᵒᵖ) ↦
                    AddEquiv.toAddCommGrpIso
                      (let __Equiv :
                        (↑(Functor.obj
                                (shiftFunctor Cᵒᵖ (m + 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' (m + n) a a'' ⋯));
                      { toEquiv := __Equiv, map_add' := ⋯ }))
                  ⋯))
              x_1) :
          (a : (↑((shiftFunctor Cᵒᵖ (m + n) ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x_1) : Type v_1)) →
            (↑((preadditiveYoneda.obj ((shiftFunctor C a'').obj B)).obj x_1) : Type v_1))
        x :
      (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') B)) x_1) :
        Type v_1))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              (Iso.hom
                (Functor.isoWhiskerRight (shiftFunctorAdd Cᵒᵖ m n)
                    (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) ≪≫
                  Functor.associator (shiftFunctor Cᵒᵖ m) (shiftFunctor Cᵒᵖ n)
                      (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) B)) ≪≫
                    Functor.isoWhiskerLeft (shiftFunctor Cᵒᵖ m)
                        (NatIso.ofComponents
                          (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' ha'));
                              { 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) :
                                    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) }))
                          ⋯) ≪≫
                      NatIso.ofComponents
                        (fun (A : Cᵒᵖ) ↦
                          AddEquiv.toAddCommGrpIso
                            (let __Equiv :
                              (↑(Functor.obj
                                      (shiftFunctor Cᵒᵖ m ⋙
                                        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' m a' a'' ha''));
                            { toEquiv := __Equiv, map_add' := ⋯ }))
                        ⋯))
              x_1) :
          (a : (↑((shiftFunctor Cᵒᵖ (m + n) ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x_1) : Type v_1)) →
            (↑((preadditiveYoneda.obj ((shiftFunctor C a'').obj B)).obj x_1) : Type v_1))
        x :
      (↑(Functor.obj (Functor.obj preadditiveYoneda (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') B)) x_1) :
        Type v_1))

Tactic:
exact ShiftedHom.opEquiv'_add_symm n m a a' a'' ha' ha'' x.op

Premises used: Quiver.Hom.op, CategoryTheory.ShiftedHom.opEquiv'_add_symm