-- 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
n : ℤ
hmn : -n + n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
    (Functor.map (shiftFunctor Cᵒᵖ (-n))
      (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯))
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
        (Opposite.op
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X))))))
      (Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯))
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯))
          (Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
              (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X))))))
      (Functor.map (shiftFunctor Cᵒᵖ n)
          (Quiver.Hom.op
            (Functor.map (shiftFunctor C n)
              (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n hmn)) (Opposite.op X))))) ≫
        Functor.map (shiftFunctor Cᵒᵖ n)
            (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n hmn))
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))) ≫
          NatTrans.app (Iso.inv (shiftFunctorComm Cᵒᵖ n (-n)))
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
have simp : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n))
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
  (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n sorry)) (Opposite.op X) ≫
    CategoryStruct.comp (Y :=
      Opposite.op
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))
      (Quiver.Hom.op
        (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n sorry))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
      (Quiver.Hom.op
          (Functor.map (shiftFunctor C n)
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) sorry))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n sorry))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))))
  (CategoryStruct.comp (Y :=
    Opposite.op
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X))))))
    (Quiver.Hom.op
      (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) sorry))
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))))
    (Quiver.Hom.op
        (Functor.map (shiftFunctor C (-n))
          (Functor.map (shiftFunctor C n)
            (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n hmn)) (Opposite.op X))))) ≫
      Quiver.Hom.op
          (Functor.map (shiftFunctor C (-n))
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n hmn))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
        Quiver.Hom.op
            (Functor.map (shiftFunctor C (-n))
              (Quiver.Hom.unop
                (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n sorry))
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
          Quiver.Hom.op
              (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) sorry))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
            CategoryStruct.comp (Y :=
              Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n) ⋙ shiftFunctor C n)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
              (Quiver.Hom.op
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n sorry))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
              (Quiver.Hom.op
                  (Functor.map (shiftFunctor C n)
                    (Quiver.Hom.unop
                      (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) sorry))
                        (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))) ≫
                NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n sorry))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                    (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))))))
Tactic: simp only [shiftFunctor_op_map _ (-n) n, shiftFunctor_op_map _ n (-n),
    shiftFunctorComm_inv_app_of_add_eq_zero n (-n) (by lia), assoc,
    shiftFunctorCompIsoId_op_inv_app, shiftFunctorCompIsoId_op_hom_app,
    shift_shiftFunctorCompIsoId_hom_app, op_comp, unop_comp, Quiver.Hom.unop_op,
    Functor.map_comp, Iso.inv_hom_id_app_assoc, Functor.op_obj]