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