-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
⊢ Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D (a + b)) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E (a + b)) (F'.obj (L.obj X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (L.obj X)) ≫
      CategoryStruct.comp (Y :=
        F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
        (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
        (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
            (Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C (a + b)) X) ≫
              F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
                NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
                  map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
                    NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                      map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (L.obj X)) ≫
      CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))))
        (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
          (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X)))
        (CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
          (map (shiftFunctor E b) (F'.map (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
          (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
            CategoryStruct.comp (Y :=
              obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
              (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
              (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
have w : Eq (α :=
  F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))) ⟶
    obj.{v₃, v₃, u₃, u₃} (shiftFunctor E (a + b)) (F'.obj (L.obj X)))
  (CategoryStruct.comp (Y :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
    (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
        (Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C (a + b)) X) ≫
          F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
            NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
              map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                  map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)))
  (CategoryStruct.comp (Y :=
    obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
      (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X)))
    (CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
      (map (shiftFunctor E b) (F'.map (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
      (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
Tactic: congr 1