-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
rw :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₃) X)
      (NatTrans.app
        (Iso.hom
          (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
            (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ ⋯))
        X)
      (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (Functor.map
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (NatTrans.app
              (Iso.inv
                (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ ⋯))
              X))))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (NatTrans.app
        (Iso.hom
          (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
            (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ ⋯))
        X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, 0} C ℤ) b₁ b₂ b₃ ⋯)) X ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
          (Functor.map
            (shiftFunctor
              (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
              a₂)
            (NatTrans.app
              (Iso.inv
                (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                  (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ ⋯))
              X)))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))

Tactic:
rw [oppositeShiftFunctorAdd'_hom_app]

Premises used: CategoryTheory.oppositeShiftFunctorAdd'_hom_app