-- 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 b : A
h : a + b = 0
inst_5 : G.CommShift A
Y : C
⊢ Eq (α := (F ⋙ shiftFunctor D a).obj Y ⟶ (shiftFunctor C a ⋙ F).obj Y) (NatTrans.app (Iso.inv (iso adj a)) Y)
    (CategoryStruct.comp (Y :=
      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 ⋙ shiftFunctor C b) Y)))
      (Functor.map (shiftFunctor D a) (F.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a b h)) Y)))
      (Functor.map (shiftFunctor D a)
          (F.map
            (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
            (F.obj ((shiftFunctor D b ⋙ G).obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))))
          (Functor.map (shiftFunctor D a)
            (F.map
              (NatTrans.app (Iso.inv (Functor.commShiftIso G b))
                (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))))
          (Functor.map (shiftFunctor D a)
              (adj.counit.app
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
                  (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))) ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId D b a ⋯))
              (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))))
have obtain : ∀ (h : a + -a = 0),
  Eq (α := (F ⋙ shiftFunctor D a).obj Y ⟶ (shiftFunctor C a ⋙ F).obj Y) (NatTrans.app (Iso.inv (iso adj a)) Y)
    (CategoryStruct.comp (Y :=
      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 ⋙ shiftFunctor C (-a)) Y)))
      (Functor.map (shiftFunctor D a) (F.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a (-a) h)) Y)))
      (Functor.map (shiftFunctor D a)
          (F.map
            (Functor.map (shiftFunctor C (-a))
              (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
            (F.obj ((shiftFunctor D (-a) ⋙ G).obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))))
          (Functor.map (shiftFunctor D a)
            (F.map
              (NatTrans.app (Iso.inv (Functor.commShiftIso G (-a)))
                (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))))
          (Functor.map (shiftFunctor D a)
              (adj.counit.app
                (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) Y)))) ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-a) a sorry))
              (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))))
Tactic: obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
Cleared hypotheses: b, h