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