-- 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
a₁ :
  Eq (α :=
    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))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-a))
              (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))))
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))))
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-a) a ⋯))
              (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
a₂ :
  Eq (α :=
    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))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)) ≫
        Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
a₃ :
  Eq (α :=
    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))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X ≫
      Functor.map (shiftFunctor D a) (F.map (adj.unit.app X)) ≫
        Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
a₄ :
  Eq (α :=
    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))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X ≫
      Functor.map (shiftFunctor D a) (F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α :=
    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))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
have a₅ : Eq (α :=
  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))
  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X ≫ Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: rw [shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app_assoc,
    Functor.commShiftIso_hom_naturality_assoc, ← Functor.map_comp,
    left_triangle_components, Functor.map_id, comp_id]