-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y Z : C
inst_7 : W.IsCompatibleWithShift M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M X Z
inst_11 : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C c) Z))
        (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
          ((SmallHom.equiv W L :
              (a_1 : SmallHom W X ((shiftFunctor C a).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y))
            f)
          ((SmallHom.equiv W L :
              (a_1 : SmallHom W ((shiftFunctor C a).obj Y) ((shiftFunctor C c).obj Z)) →
                L.obj ((shiftFunctor C a).obj Y) ⟶ L.obj ((shiftFunctor C c).obj Z))
            (g.shift (W := W) a c h)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L c)) Z) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
    (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
        (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
            ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
            (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) :
          L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
        (Functor.map (shiftFunctor D a)
              (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z))
                ((SmallHom.equiv W L : (a : SmallShiftedHom W Y Z b) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z)) g)
                (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z) :
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y) ⟶
            Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z)) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
have simp : Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
      ((SmallHom.equiv W L :
          (a_1 : SmallHom W X ((shiftFunctor C a).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y))
        f)
      (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z)))
          (Functor.map (shiftFunctor D a)
            ((SmallHom.equiv W L :
                (a : SmallHom W Y ((shiftFunctor C b).obj Z)) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z))
              g))
          (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z)))) :
    L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
      ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
      (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z)))
          (Functor.map (shiftFunctor D a)
            ((SmallHom.equiv W L : (a : SmallShiftedHom W Y Z b) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z)) g))
          (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z)))) :
    L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
Tactic: simp only [equiv_shift', Functor.comp_obj, assoc, Iso.inv_hom_id_app,
    comp_id, Functor.map_comp]