-- 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} (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))
have a₁ : adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
    G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
  e₂.hom.app 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))) ≫
      G.map (e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))
Tactic: rw [adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp, adj.unit_naturality_assoc, ← eq]