-- 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₁ Z₁ : C₁
X₂ Y₂ Z₂ : 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₂
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z₁ ≅ Z₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
inst_12 : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst_13 : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst_14 : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst_15 : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst_16 : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst_17 : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
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 Z₂) c)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eX.inv ≫ e.hom.app X₁))
        (ShiftedHom.comp
          (ShiftedHom.comp (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj Y₁))
            (ShiftedHom.map
              ((SmallShiftedHom.equiv W₁ W₁.Q :
                  (a_1 : SmallShiftedHom W₁ X₁ Y₁ a) → ShiftedHom (W₁.Q.obj X₁) (W₁.Q.obj Y₁) a)
                f)
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
            (ShiftedHom.map
              ((SmallShiftedHom.equiv W₁ W₁.Q :
                  (a : SmallShiftedHom W₁ Y₁ Z₁ b) → ShiftedHom (W₁.Q.obj Y₁) (W₁.Q.obj Z₁) b)
                g)
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
            h)
          (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) ⋯)
        ⋯ :
      ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
    (ShiftedHom.comp (Y := W₂.Q.obj Y₂)
        (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eX.inv ≫ e.hom.app X₁))
          (ShiftedHom.comp
            (ShiftedHom.map
              ((SmallShiftedHom.equiv W₁ W₁.Q :
                  (a_1 : SmallShiftedHom W₁ X₁ Y₁ a) → ShiftedHom (W₁.Q.obj X₁) (W₁.Q.obj Y₁) a)
                f)
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
            (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ W₂.Q.map eY.hom)) ⋯)
          ⋯)
        (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eY.inv ≫ e.hom.app Y₁))
          (ShiftedHom.comp
            (ShiftedHom.map
              ((SmallShiftedHom.equiv W₁ W₁.Q :
                  (a : SmallShiftedHom W₁ Y₁ Z₁ b) → ShiftedHom (W₁.Q.obj Y₁) (W₁.Q.obj Z₁) b)
                g)
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
            (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) ⋯)
          ⋯)
        h :
      ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
have a₁ : Eq (α := ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
  (ShiftedHom.comp (ShiftedHom.mk₀ 0 sorry (W₂.Q.map eX.inv ≫ e.hom.app X₁))
      (ShiftedHom.comp (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj Y₁)) (a := a) (b := b)
        (ShiftedHom.map
          ((SmallShiftedHom.equiv W₁ W₁.Q :
              (a_1 : SmallShiftedHom W₁ X₁ Y₁ a) → ShiftedHom (W₁.Q.obj X₁) (W₁.Q.obj Y₁) a)
            f)
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((SmallShiftedHom.equiv W₁ W₁.Q :
                (a : SmallShiftedHom W₁ Y₁ Z₁ b) → ShiftedHom (W₁.Q.obj Y₁) (W₁.Q.obj Z₁) b)
              g)
            (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
          (ShiftedHom.mk₀ 0 sorry (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) sorry)
        sorry)
      sorry :
    ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
  (ShiftedHom.comp (ShiftedHom.mk₀ 0 sorry (W₂.Q.map eX.inv ≫ e.hom.app X₁))
      (ShiftedHom.comp (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj (W₁.Q.obj Y₁)) (a := a) (b := b)
        (ShiftedHom.map
          ((SmallShiftedHom.equiv W₁ W₁.Q :
              (a_1 : SmallShiftedHom W₁ X₁ Y₁ a) → ShiftedHom (W₁.Q.obj X₁) (W₁.Q.obj Y₁) a)
            f)
          (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
        (ShiftedHom.comp (a := 0) (b := b)
          (ShiftedHom.mk₀ 0 sorry ((e.inv.app Y₁ ≫ W₂.Q.map eY.hom) ≫ W₂.Q.map eY.inv ≫ e.hom.app Y₁))
          (ShiftedHom.comp
            (ShiftedHom.map
              ((SmallShiftedHom.equiv W₁ W₁.Q :
                  (a : SmallShiftedHom W₁ Y₁ Z₁ b) → ShiftedHom (W₁.Q.obj Y₁) (W₁.Q.obj Z₁) b)
                g)
              (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q))
            (ShiftedHom.mk₀ 0 sorry (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) sorry)
          sorry)
        sorry)
      sorry :
    ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
Tactic: rw [ShiftedHom.comp_assoc _ _ _ _ (zero_add b) (by simpa),
    ShiftedHom.comp_assoc _ _ _ _ h (by simpa),
    ShiftedHom.comp_assoc _ _ _ _ (add_zero b) (by simpa),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero 0) (add_zero b) (by simp),
    ShiftedHom.mk₀_comp_mk₀]