-- 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
E : Type u_4
inst_5 : Category.{v_3, u_4} E
inst_6 : HasShift.{v_3, u_4, u_3} E A
G : Functor.{v_2, v_3, u_2, u_4} D E
inst_7 : F.CommShift A
inst_8 : G.CommShift A
x : A
x_1 : OppositeShift.{v_1, u_1, u_3} C A
w :
  Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_3, u_4, u_3} E A)
      (Functor.obj (OppositeShift.functor A (F ⋙ G))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
      (Functor.obj.{v_3, v_3, u_4, u_4} (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
        (Functor.obj (C := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A G)
          (Functor.obj (OppositeShift.functor A F) x_1))))
    (Quiver.Hom.op (app (Iso.inv (Functor.commShiftIso (F ⋙ G) x)) (Opposite.unop x_1)) ≫
        Functor.map (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
          (𝟙 (Functor.obj (OppositeShift.functor A (F ⋙ G)) x_1)) :
      Quiver.Hom (V := OppositeShift.{v_3, u_4, u_3} E A)
        (Functor.obj (OppositeShift.functor A (F ⋙ G))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
        (Functor.obj.{v_3, v_3, u_4, u_4} (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
          (Functor.obj (C := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A G)
            (Functor.obj (OppositeShift.functor A F) x_1))))
    (𝟙
          (Functor.obj (OppositeShift.functor A (F ⋙ G))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1)) ≫
        app
          (Iso.hom
            (Functor.commShiftIso
              (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F)
                (OppositeShift.functor A G))
              x))
          x_1 :
      Quiver.Hom (V := OppositeShift.{v_3, u_4, u_3} E A)
        (Functor.obj (OppositeShift.functor A (F ⋙ G))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x) x_1))
        (Functor.obj.{v_3, v_3, u_4, u_4} (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
          (Functor.obj (C := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A G)
            (Functor.obj (OppositeShift.functor A F) x_1))))
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_3, u_4, u_3} E A)
      (Functor.obj (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x ⋙ OppositeShift.functor A (F ⋙ G)) x_1)
      (Functor.obj
        (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F) (OppositeShift.functor A G) ⋙
          shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x)
        x_1))
    (app
      (Iso.hom (Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x) ≫
        Functor.whiskerRight (Iso.hom (OppositeShift.natIsoComp A F G))
          (shiftFunctor (OppositeShift.{v_3, u_4, u_3} E A) x))
      x_1)
    (app
      (Functor.whiskerLeft (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) x)
          (Iso.hom (OppositeShift.natIsoComp A F G)) ≫
        Iso.hom
          (Functor.commShiftIso
            (Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F)
              (OppositeShift.functor A G))
            x))
      x_1)

Tactic:
dsimp [OppositeShift.natIsoComp, Functor.commShiftOp_iso_eq]

Premises used: CategoryTheory.Functor.commShiftOp_iso_eq, CategoryTheory.NatTrans.OppositeShift.natIsoComp