-- 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))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Z c) → L.obj X ⟶ L.obj ((shiftFunctor C c).obj Z))
          (SmallHom.comp (W := W) f (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 erw : 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))
Tactic: erw [SmallHom.equiv_comp]