-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))))
        (Functor.map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a (-a) ⋯)) (G.obj (F.obj X))))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))))
          (Functor.map (shiftFunctor C a)
            (Functor.map (shiftFunctor C (-a)) (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) (F.obj X))))
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (G.obj
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-a))
                  (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))))
            (Functor.map (shiftFunctor C a)
              (NatTrans.app (Iso.inv (Functor.commShiftIso G (-a)))
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
            (Functor.map (shiftFunctor C a)
                (NatTrans.app (Iso.hom (Functor.commShiftIso G (-a)))
                  (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-a) a ⋯))
                  (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))))
have slice_rhs : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (Functor.map (shiftFunctor C a) (adj.unit.app X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))))
        (Functor.map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a (-a) sorry)) (G.obj (F.obj X))))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))))
          (Functor.map (shiftFunctor C a)
            (Functor.map (shiftFunctor C (-a)) (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) (F.obj X))))
          (CategoryStruct.comp (Y := G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
            (Functor.map (shiftFunctor C a)
                (𝟙 ((G ⋙ shiftFunctor C (-a)).obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-a) a sorry))
                (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
            (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
Tactic: slice_rhs 4 5 => rw [← Functor.map_comp, Iso.inv_hom_id_app]