-- 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} (α :=
    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)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (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)) ⟶
        Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop
            (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (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)) ⟶
        Opposite.unop X)
a₁ :
  Eq.{v_1 + 1} (α :=
    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)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (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)) ⟶
        Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X) ≫
            Quiver.Hom.unop (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)))) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (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)) ⟶
        Opposite.unop X)
a₂ :
  Eq.{v_1 + 1} (α :=
    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)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (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)) ⟶
        Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0)
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X) ≫
            NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (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)) ⟶
        Opposite.unop X)
a₃ :
  Eq.{v_1 + 1} (α :=
    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)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (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)) ⟶
        Opposite.unop X)
    ((Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
          Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (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)) ⟶
        Opposite.unop X)
a₄ :
  Eq.{v_1 + 1} (α :=
    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)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
      Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X))
    ((Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X))
⊢ Eq.{v_1 + 1} (α :=
    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)) ⟶
      Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) (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)) ⟶
        Opposite.unop X)
    (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (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)) ⟶
        Opposite.unop X)
have a₅ : Eq.{v_1 + 1} (α :=
  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)) ⟶
    Opposite.unop X)
  (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X)) ≫
    Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X))
  (Functor.map (shiftFunctor C (A := ℤ) 0) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X)) ≫
    Functor.map (shiftFunctor C (A := ℤ) 0) (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X))
Tactic: rw [shiftFunctorZero_op_inv_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_hom_app, assoc]