-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangle (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T₁ T₂ : (Triangle.{v_1, u_1} C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ Eq.{v_1 + 1} (α :=
    Opposite.op (Opposite.unop T₁).obj₁ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃))
        (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
                (Opposite.op (Opposite.unop T₁).obj₁) :
              Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₁).obj₁) ⟶
                Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                  (Opposite.op (Opposite.unop T₁).obj₁))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₁).mor₃.op :
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)) ⟶
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃)) :
          Opposite.op (Opposite.unop T₁).obj₁ ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃))
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) φ.unop.hom₃.op :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃)) :
      Opposite.op (Opposite.unop T₁).obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
    (φ.unop.hom₁.op ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₂).obj₁)))
          (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
              (Opposite.op (Opposite.unop T₂).obj₁) :
            Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₂).obj₁) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Opposite.unop T₂).obj₁))
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₂).obj₁)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃)) :
      Opposite.op (Opposite.unop T₁).obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
have rw : Eq.{v_1 + 1} (α :=
  Opposite.op (Opposite.unop T₁).obj₁ ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
  (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)))
      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
          (Opposite.op (Opposite.unop T₁).obj₁) :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₁).obj₁) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Opposite.unop T₁).obj₁))
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₂).obj₁)))
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) φ.unop.hom₁)))
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃)) :
    Opposite.op (Opposite.unop T₁).obj₁ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
  (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (opShiftFunctorEquivalence C 1))
        (Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (opShiftFunctorEquivalence C 1))
          (Opposite.op (Opposite.unop T₁).obj₁)))
      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
          (Opposite.op (Opposite.unop T₁).obj₁) :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₁).obj₁) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙ Equivalence.functor (opShiftFunctorEquivalence C 1))
            (Opposite.op (Opposite.unop T₁).obj₁))
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (opShiftFunctorEquivalence C 1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (opShiftFunctorEquivalence C 1))
            (Opposite.op (Opposite.unop T₂).obj₁)))
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) φ.unop.hom₁.op.unop)))
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op)) :
    Opposite.op (Opposite.unop T₁).obj₁ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
Tactic: rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp,
          opShiftFunctorEquivalence_counitIso_inv_naturality_assoc]