-- 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 : C
inst_7 : W.IsCompatibleWithShift M
a : M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a') Y))
        ((SmallHom.equiv W L :
            (a : SmallShiftedHom W ((shiftFunctor C n).obj X) Y a') →
              L.obj ((shiftFunctor C n).obj X) ⟶ L.obj ((shiftFunctor C a').obj Y))
          (f.shift (W := W) n a' h))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L a')) Y) :
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))
    (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj X))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
        (Functor.map (shiftFunctor D n)
            (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)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y)) :
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))
have erw : Eq (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a') Y))
    (CategoryStruct.comp (Y := (L ⋙ shiftFunctor D n).obj X) (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y)))
        (Functor.map (shiftFunctor D n)
          ((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))
        (Functor.map (shiftFunctor D n) (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y) ≫
            NatTrans.app (Iso.inv (Functor.commShiftIso L a')) Y)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso L a')) Y))
  (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj X))
    (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
    (Functor.map (shiftFunctor D n)
        (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)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y)))
Tactic: erw [equiv_shift']