-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
m : M
f : ShiftedHom X₁ Y₁ m
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
⊢ Eq (α := ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
    (W₂.Q.map eX.inv ≫
      e.hom.app X₁ ≫
        (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map (W₁.Q.map f) ≫
          CategoryStruct.comp (Y :=
            (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj
              (Functor.obj (shiftFunctor W₁.Localization m) (W₁.Q.obj Y₁)))
            ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map
              (NatTrans.app (Iso.hom (Functor.commShiftIso W₁.Q m)) Y₁))
            (CategoryStruct.comp (Y :=
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj
                (W₁.Q.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
              ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map
                (NatTrans.app (Iso.inv (Functor.commShiftIso W₁.Q m)) Y₁))
              (e.inv.app (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁) ≫
                CategoryStruct.comp (Y :=
                  W₂.Q.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
                  (W₂.Q.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
                  (NatTrans.app (Iso.hom (Functor.commShiftIso W₂.Q m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
                    Functor.map (shiftFunctor W₂.Localization m) (W₂.Q.map eY.hom)))))
    (W₂.Q.map eX.inv ≫
      W₂.Q.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map f) ≫
        CategoryStruct.comp (Y :=
          W₂.Q.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
          (W₂.Q.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
          (NatTrans.app (Iso.hom (Functor.commShiftIso W₂.Q m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
            Functor.map (shiftFunctor W₂.Localization m) (W₂.Q.map eY.hom)))
have a : Eq (α := ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
  (W₂.Q.map eX.inv ≫
    e.hom.app X₁ ≫
      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map (W₁.Q.map f) ≫
        CategoryStruct.comp (Y :=
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj
            (W₁.Q.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
          ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map
            (CategoryStruct.comp (Y := Functor.obj (shiftFunctor W₁.Localization m) (W₁.Q.obj Y₁))
              (NatTrans.app (Iso.hom (Functor.commShiftIso W₁.Q m)) Y₁)
              (NatTrans.app (Iso.inv (Functor.commShiftIso W₁.Q m)) Y₁)))
          (e.inv.app (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁) ≫
            CategoryStruct.comp (Y :=
              W₂.Q.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
              (W₂.Q.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
              (NatTrans.app (Iso.hom (Functor.commShiftIso W₂.Q m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
                Functor.map (shiftFunctor W₂.Localization m) (W₂.Q.map eY.hom))))
  (W₂.Q.map eX.inv ≫
    W₂.Q.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map f) ≫
      CategoryStruct.comp (Y :=
        W₂.Q.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
        (W₂.Q.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
        (NatTrans.app (Iso.hom (Functor.commShiftIso W₂.Q m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
          Functor.map (shiftFunctor W₂.Localization m) (W₂.Q.map eY.hom)))
Tactic: nth_rw 2 [← Functor.map_comp_assoc]