-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
a b : A
x : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (obj
            (OppositeShift.functor A F :
              Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
        (Quiver.Hom.unop
            (map (OppositeShift.functor A F)
              (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (Opposite.unop (Opposite.op x))))) :
          Opposite.unop (Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x))) ⟶
            Opposite.unop
              (obj
                (OppositeShift.functor A F :
                  Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
        (CategoryStruct.comp (Y :=
            Opposite.unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                (obj
                  (OppositeShift.functor A F :
                    Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                      (OppositeShift.{v_2, u_2, u_3} D A))
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
            (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) b))
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x))) :
              Opposite.unop
                  (obj
                    (OppositeShift.functor A F :
                      Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                        (OppositeShift.{v_2, u_2, u_3} D A))
                    (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))) ⟶
                Opposite.unop
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                    (obj
                      (OppositeShift.functor A F :
                        Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                          (OppositeShift.{v_2, u_2, u_3} D A))
                      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
            (Quiver.Hom.unop
                  (map (shiftFunctor Dᵒᵖ b)
                    (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) a)) (Opposite.op x))) ≫
                Quiver.Hom.unop
                  (Quiver.Hom.op
                    (NatTrans.app (Iso.inv (shiftFunctorAdd D a b))
                      (Opposite.unop
                        (obj
                          (OppositeShift.functor A F :
                            Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                              (OppositeShift.{v_2, u_2, u_3} D A))
                          (Opposite.op x))))) :
              Opposite.unop
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                    (obj
                      (OppositeShift.functor A F :
                        Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                          (OppositeShift.{v_2, u_2, u_3} D A))
                      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))) ⟶
                obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x)) :
          Opposite.unop
              (obj
                (OppositeShift.functor A F :
                  Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) x) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) x)))
          (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) b))
              (Opposite.op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) x))))
          (map (shiftFunctor D b)
              (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) a)) (Opposite.op x))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (obj
            (OppositeShift.functor A F :
              Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
        (Quiver.Hom.unop
            (map (OppositeShift.functor A F) (NatTrans.app (Iso.inv (shiftFunctorAdd Cᵒᵖ a b)) (Opposite.op x))) :
          Opposite.unop (Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x))) ⟶
            Opposite.unop
              (obj
                (OppositeShift.functor A F :
                  Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
        (CategoryStruct.comp (Y :=
            Opposite.unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                (obj
                  (OppositeShift.functor A F :
                    Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                      (OppositeShift.{v_2, u_2, u_3} D A))
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))))
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) b))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x))))
            (CategoryStruct.comp (Y :=
              Opposite.unop
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ b)
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ a)
                    (obj
                      (OppositeShift.functor A F :
                        Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                          (OppositeShift.{v_2, u_2, u_3} D A))
                      (Opposite.op x)))))
              (Quiver.Hom.unop
                (map (shiftFunctor Dᵒᵖ b)
                  (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) a)) (Opposite.op x))))
              (Quiver.Hom.unop
                (NatTrans.app (Iso.hom (shiftFunctorAdd Dᵒᵖ a b))
                  (obj
                    (OppositeShift.functor A F :
                      Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                        (OppositeShift.{v_2, u_2, u_3} D A))
                    (Opposite.op x))))) :
          Opposite.unop
              (obj
                (OppositeShift.functor A F :
                  Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ b)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a) (Opposite.op x)))) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) x) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) x)))
          (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) b))
              (Opposite.op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) x))))
          (map (shiftFunctor D b)
              (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso (OppositeShift.functor A F) a)) (Opposite.op x))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj x)) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj x))

Tactic:
erw [oppositeShiftFunctorAdd_hom_app, oppositeShiftFunctorAdd_inv_app]

Premises used: CategoryTheory.oppositeShiftFunctorAdd_inv_app, CategoryTheory.oppositeShiftFunctorAdd_hom_app