-- 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
a : A
inst_5 : F.CommShift A
Y : D
h : -a + a = 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y) ⟶
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        CategoryStruct.comp (Y :=
          G.obj
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
              (F.obj
                (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 Y))))))
          (G.map
            (Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.inv (Functor.commShiftIso F (-a)))
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
          (CategoryStruct.comp (Y :=
            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 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))))
            (G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (Functor.commShiftIso F (-a)))
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))))
            (G.map
                (Functor.map (shiftFunctor D a)
                  (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
              G.map
                  (Functor.map (shiftFunctor D a)
                    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj Y)))) ≫
                G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a h))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
        G.map
            (Functor.map (shiftFunctor D a)
              (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
          G.map
              (Functor.map (shiftFunctor D a)
                (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj Y)))) ≫
            G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
have slice_lhs : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y) ⟶
    G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
    G.map
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a sorry))
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
      ((G.map
              (Functor.map (shiftFunctor D a)
                (𝟙 ((F ⋙ shiftFunctor D (-a)).obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))) ≫
            G.map
              (Functor.map (shiftFunctor D a)
                (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y))))) ≫
          G.map
            (Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj Y))))) ≫
        G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
    G.map
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a h))
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))) ≫
      G.map
          (Functor.map (shiftFunctor D a)
            (Functor.map (shiftFunctor D (-a)) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj Y)))) ≫
        G.map
            (Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj Y)))) ≫
          G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y)))
Tactic: slice_lhs 3 4 => rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]