-- 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 : F.CommShift A
a : A
X : C
⊢ Eq.{v_2 + 1} (α :=
    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} (𝟭 C) X)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (((Equiv.symm
              (adj.homEquiv
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
            Equiv.{v_1 + 1, v_2 + 1}
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
                G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
              (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} (𝟭 C) X)) ⟶
                Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
          (a_1 : (shiftFunctor C a).obj ((𝟭 C).obj X) ⟶ G.obj ((shiftFunctor D a).obj (F.obj X))) →
            F.obj ((shiftFunctor C a).obj ((𝟭 C).obj X)) ⟶ (shiftFunctor D a).obj (F.obj X))
        (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
          adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))) ≫
            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 (F.obj X))))) ≫
              G.map
                  (Functor.map (shiftFunctor D a)
                    (Functor.map (shiftFunctor D (-a))
                      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))) ≫
                G.map
                    (Functor.map (shiftFunctor D a)
                      (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X))))) ≫
                  G.map (Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))) :
      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} (𝟭 C) X)) ⟶
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (((Equiv.symm
              (adj.homEquiv
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
            Equiv.{v_1 + 1, v_2 + 1}
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
                G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
              (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} (𝟭 C) X)) ⟶
                Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
          (a_1 : (shiftFunctor C a).obj ((𝟭 C).obj X) ⟶ G.obj ((shiftFunctor D a).obj (F.obj X))) →
            F.obj ((shiftFunctor C a).obj ((𝟭 C).obj X)) ⟶ (shiftFunctor D a).obj (F.obj X))
        (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj X))) :
      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} (𝟭 C) X)) ⟶
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
have a₁ : Eq.{v_2 + 1} (α :=
  F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
  (((Equiv.symm
            (adj.homEquiv (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)
              (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
          Equiv.{v_1 + 1, v_2 + 1}
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
              G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
              Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
        (a_1 : (shiftFunctor C a).obj X ⟶ G.obj ((shiftFunctor D a).obj (F.obj X))) →
          F.obj ((shiftFunctor C a).obj X) ⟶ (shiftFunctor D a).obj (F.obj X))
      (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
        adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))) ≫
          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 (F.obj X))))) ≫
            G.map
                (Functor.map (shiftFunctor D a)
                  (Functor.map (shiftFunctor D (-a))
                    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X))))) ≫
              G.map
                  (Functor.map (shiftFunctor D a)
                    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj (G.obj (F.obj X))))) ≫
                G.map (Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))) :
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
  (((Equiv.symm
            (adj.homEquiv (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)
              (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
          Equiv.{v_1 + 1, v_2 + 1}
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
              G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
            (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
              Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) :
        (a_1 : (shiftFunctor C a).obj X ⟶ G.obj ((shiftFunctor D a).obj (F.obj X))) →
          F.obj ((shiftFunctor C a).obj X) ⟶ (shiftFunctor D a).obj (F.obj X))
      (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        G.map (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
          𝟙 (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) :
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
Tactic: dsimp