-- 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 :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop
            (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
              Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
a₁ :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
            Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
a₂ :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
            Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
a₃ :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
          Functor.map (shiftFunctor C (A := ℤ) 0)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
a₄ :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0) (Opposite.unop X)))
      (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))
      (Functor.map (shiftFunctor C (A := ℤ) 0)
        (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X))))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)))
a₅ a₆ :
  Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0) (Opposite.unop X))
      (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0) (Opposite.unop X)))
        (Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))
        (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)))))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)))
⊢ Eq.{v_1 + 1} (α :=
    Opposite.unop X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))
    (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X)) :
      Opposite.unop X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)))

Tactic:
rw [shiftFunctorZero_op_hom_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_inv_app, assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app, CategoryTheory.Functor.map_comp, CategoryTheory.shiftFunctorCompIsoId_zero_zero_inv_app