-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (m + n)) (Opposite.op X)
simp :
  Eq (α := ShiftedHom X Y a'')
    ((Quiver.Hom.unop
          (CategoryStruct.comp (Y :=
            Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n))
                (Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m ⋙ shiftFunctor Cᵒᵖ n) (Opposite.op X)))))
            (Quiver.Hom.op
              (Functor.map (shiftFunctor C (m + n))
                (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯)) (Opposite.op X)))))
            (Quiver.Hom.op
                (NatTrans.app (Iso.inv (shiftFunctorAdd' C n m (m + n) ⋯))
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m ⋙ shiftFunctor Cᵒᵖ n) (Opposite.op X)))) ≫
              CategoryStruct.comp (Y :=
                Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
                    (Opposite.unop
                      (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ)
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))))
                (Quiver.Hom.op
                    (Functor.map (shiftFunctor C m)
                      (Quiver.Hom.unop
                        (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))) :
                  Opposite.op
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
                        (Opposite.unop
                          (Functor.obj.{v_1, v_1, u_1, u_1}
                            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙
                              Equivalence.inverse (opShiftFunctorEquivalence C n))
                            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))) ⟶
                    Opposite.op
                      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m)
                        (Opposite.unop
                          (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ)
                            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X))))))
                (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m))) (Opposite.op X) :
                  Functor.obj.{v_1, v_1, u_1, u_1}
                      (Equivalence.functor (opShiftFunctorEquivalence C m) ⋙
                        Equivalence.inverse (opShiftFunctorEquivalence C m))
                      (Opposite.op X) ⟶
                    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)))) ≫
        Functor.map (shiftFunctor C (m + n)) x.unop) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a (m + n) a'' ⋯)) Y)
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C m) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C m))
            (Opposite.op X)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C m))) (Opposite.op X)))
        (Functor.map (shiftFunctor C m)
          (Quiver.Hom.unop
            (Quiver.Hom.op
              (CategoryStruct.comp (Y :=
                  Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1}
                      (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙
                        Equivalence.inverse (opShiftFunctorEquivalence C n))
                      (Opposite.op
                        (Functor.obj.{v_1, v_1, u_1, u_1}
                          (shiftFunctor C
                            ((Discrete.addMonoidalFunctor
                                    (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n)
                                      CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux._proof_1✝)).obj
                                { as := m : Discrete ℤ }).as)
                          X))))
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                      (Opposite.op
                        (Functor.obj.{v_1, v_1, u_1, u_1}
                          (shiftFunctor C
                            ((Discrete.addMonoidalFunctor
                                    (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n)
                                      CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux._proof_1✝)).obj
                                { as := m : Discrete ℤ }).as)
                          X))))
                  (Functor.map (shiftFunctor C n)
                    (Quiver.Hom.unop (x ≫ NatTrans.app (Iso.hom (shiftFunctorAdd Cᵒᵖ m n)) (Opposite.op X)))) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y)))) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a' m a'' ⋯)) Y)
⊢ Eq (α := ShiftedHom X Y a'')
    ((Equiv.symm (opEquiv' (m + n) a a'' ⋯) :
          (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)) →
            ShiftedHom X Y a'')
        x :
      ShiftedHom X Y a'')
    ((Equiv.symm (opEquiv' m a' a'' ha'') :
          (a : Opposite.op ((shiftFunctor C a').obj Y) ⟶ (shiftFunctor Cᵒᵖ m).obj (Opposite.op X)) → ShiftedHom X Y a'')
        (Quiver.Hom.op
            ((Equiv.symm (opEquiv' n a a' ha') :
                (a :
                    Opposite.op ((shiftFunctor C a).obj Y) ⟶
                      (shiftFunctor Cᵒᵖ n).obj
                        (Opposite.op
                          ((shiftFunctor C
                                ((Discrete.addMonoidalFunctor
                                        (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n)
                                          CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux._proof_1✝)).obj
                                    { as := m }).as).obj
                            (Opposite.unop (Opposite.op X))))) →
                  ShiftedHom
                    ((shiftFunctor C
                          ((Discrete.addMonoidalFunctor
                                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n)
                                    CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux._proof_1✝)).obj
                              { as := m }).as).obj
                      (Opposite.unop (Opposite.op X)))
                    Y a')
              (x ≫ NatTrans.app (Iso.hom (shiftFunctorAdd Cᵒᵖ m n)) (Opposite.op X) :
                Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
                  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                    (Opposite.op
                      (Functor.obj.{v_1, v_1, u_1, u_1}
                        (shiftFunctor C
                          ((Discrete.addMonoidalFunctor
                                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n)
                                    CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux._proof_1✝)).obj
                              { as := m : Discrete ℤ }).as)
                        (Opposite.unop (Opposite.op X)))))) :
          Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y) ⟶
            Opposite.op
              (Functor.obj.{v_1, v_1, u_1, u_1}
                (shiftFunctor C
                  ((Discrete.addMonoidalFunctor
                          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n)
                            CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux._proof_1✝)).obj
                      { as := m : Discrete ℤ }).as)
                (Opposite.unop (Opposite.op X)))) :
      ShiftedHom X Y a'')

Tactic:
simp only [opEquiv'_symm_apply, opEquiv_symm_apply,
    opShiftFunctorEquivalence_add_unitIso_inv_app_eq _ _ _ _ (add_comm n m)]

Premises used: add_comm, CategoryTheory.ShiftedHom.opEquiv'_symm_apply, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, CategoryTheory.ShiftedHom.opEquiv_symm_apply