-- 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 (α := 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)))
have simp : Eq (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
  (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.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))))
  (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.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 : SmallShiftedHom W X Y a) → 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))))
Tactic: simp only [Functor.comp_obj, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]