-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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)))
⊢ 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)))
have 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 sorry)) 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 sorry)) X)))
Tactic: rw [shiftFunctorZero_op_hom_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_inv_app, assoc]