-- 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 : AddMonoid 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
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
⊢ Eq.{v_1 + 1} (α :=
    G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))
    (((adj.homEquiv (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
              (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) :
            Equiv.{v_2 + 1, v_1 + 1}
              (F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
                Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
                G.obj
                  (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))) :
          (a_1 : F.obj (G.obj ((shiftFunctor D a).obj Y)) ⟶ (𝟭 D).obj ((shiftFunctor D a).obj Y)) →
            G.obj ((shiftFunctor D a).obj Y) ⟶ G.obj ((𝟭 D).obj ((shiftFunctor D a).obj Y)))
        (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) :
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
        G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))
    (((adj.homEquiv (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
              (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) :
            Equiv.{v_2 + 1, v_1 + 1}
              (F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
                Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
                G.obj
                  (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))) :
          (a_1 : F.obj (G.obj ((shiftFunctor D a).obj Y)) ⟶ (𝟭 D).obj ((shiftFunctor D a).obj Y)) →
            G.obj ((shiftFunctor D a).obj Y) ⟶ G.obj ((𝟭 D).obj ((shiftFunctor D a).obj Y)))
        (F.map (e₂.hom.app Y) ≫ e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)) :
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
        G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)))
have a₁ : Eq.{v_1 + 1} (α :=
  G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
    G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
  (((adj.homEquiv (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) :
          Equiv.{v_2 + 1, v_1 + 1}
            (F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
              Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)
            (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
              G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))) :
        (a_1 : F.obj (G.obj ((shiftFunctor D a).obj Y)) ⟶ (shiftFunctor D a).obj Y) →
          G.obj ((shiftFunctor D a).obj Y) ⟶ G.obj ((shiftFunctor D a).obj Y))
      (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) :
    G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
  (((adj.homEquiv (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) :
          Equiv.{v_2 + 1, v_1 + 1}
            (F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ⟶
              Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)
            (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
              G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))) :
        (a_1 : F.obj (G.obj ((shiftFunctor D a).obj Y)) ⟶ (shiftFunctor D a).obj Y) →
          G.obj ((shiftFunctor D a).obj Y) ⟶ G.obj ((shiftFunctor D a).obj Y))
      (F.map (e₂.hom.app Y) ≫ e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y)) :
    G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y) ⟶
      G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y))
Tactic: dsimp