-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 (unop X)) =
    CategoryStruct.comp (Y :=
      F.obj
        (unop
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))
      (CategoryStruct.comp (Y :=
        unop
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
            (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))) :
          unop (op (F.obj (unop X))) ⟶
            unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))))
        (CategoryStruct.comp (Y :=
            unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                (op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))
            (Quiver.Hom.unop
                (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F n)) (unop X)))) :
              unop
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                    (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))) ⟶
                unop
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                    (op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))
            (Quiver.Hom.unop
                (NatTrans.app (Iso.hom (commShiftIso F.op n))
                  (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) :
              unop
                  (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                    (op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))) ⟶
                unop
                  (op
                    (F.obj
                      (unop
                        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                          (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))))))) :
          unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))) ⟶
            F.obj
              (unop
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                  (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))))))
      (CategoryStruct.comp (Y :=
        unop
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
            (op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.inv (commShiftIso F.op n)) (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) :
          unop
              (op
                (F.obj
                  (unop
                    (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                      (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))) ⟶
            unop
              (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                (op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))
        (CategoryStruct.comp (Y :=
          unop
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
              (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))))
          (Quiver.Hom.unop
              (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (NatTrans.app (Iso.hom (commShiftIso F n)) (unop X)))) :
            unop
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                  (op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))) ⟶
              unop
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                  (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))))
          (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))) :
            unop
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
                  (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X))))) ⟶
              unop (op (F.obj (unop X))))))
have simp : Eq.{v_2 + 1} (α := F.obj (unop X) ⟶ F.obj (unop X)) (𝟙 (F.obj (unop X)))
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))))
      (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X))) :
        obj.{v_2, v_2, u_2, u_2} (𝟭 Dᵒᵖ) (op (F.obj (unop X))) ⟶
          obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D n) ⋙ shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))
      (CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
            (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))))
          (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (𝟙 ((F ⋙ shiftFunctor D n).obj (unop X)))))
          (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))) :
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
            (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))) ⟶
          op (F.obj (unop X)))))
Tactic: simp only [map_id, assoc, ← Functor.map_comp_assoc,
    ← unop_comp, Iso.inv_hom_id_app_assoc, ← op_comp,
    Iso.inv_hom_id_app]