-- 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} (α :=
    Quiver.Hom.{v_1, u_1} (V := Cᵒᵖ)
      (Triangle.obj₃.{v_1, u_1}
        (Triangle.mk (Opposite.unop T₁).mor₂.op (Opposite.unop T₁).mor₁.op
          (CategoryStruct.comp (Y :=
            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₁))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 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)
        (Triangle.obj₁.{v_1, u_1}
          (Triangle.mk (Opposite.unop T₂).mor₂.op (Opposite.unop T₂).mor₁.op
            (CategoryStruct.comp (Y :=
              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₁))
              (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
                (Opposite.op (Opposite.unop T₂).obj₁))
              (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op))))))
    (Triangle.mor₃
        (Triangle.mk (Opposite.unop T₁).mor₂.op (Opposite.unop T₁).mor₁.op
          (CategoryStruct.comp (Y :=
            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₁))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
              (Opposite.op (Opposite.unop T₁).obj₁))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₁).mor₃.op))) ≫
      Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) φ.unop.hom₃.op)
    (φ.unop.hom₁.op ≫
      Triangle.mor₃
        (Triangle.mk (Opposite.unop T₂).mor₂.op (Opposite.unop T₂).mor₁.op
          (CategoryStruct.comp (Y :=
            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₁))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
              (Opposite.op (Opposite.unop T₂).obj₁))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op))))
have dsimp : 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₃))
Tactic: dsimp