-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst_2 : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst_3 : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₁', u₁, u₁'} C₁ D₁
L₂ : Functor.{v₂, v₂', u₂, u₂'} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
M : Type w'
inst_6 : AddMonoid M
inst_7 : HasShift.{v₁, u₁, w'} C₁ M
inst_8 : HasShift.{v₂, u₂, w'} C₂ M
inst_9 : HasShift.{v₁', u₁', w'} D₁ M
inst_10 : HasShift.{v₂', u₂', w'} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
inst_13 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_14 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_15 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_16 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_17 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
G : Functor.{v₁', v₂', u₁', u₂'} D₁ D₂
inst_18 : G.CommShift M
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
inst_19 : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
this : HasSmallLocalizedHom W₂ X₂ X₂
a :
  Eq (α := L₂.obj X₂ ⟶ L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) Y₂))
    (L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        CategoryStruct.comp (Y := G.obj (L₁.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
          (G.map
            ((SmallHom.equiv W₁ L₁ :
                (a : SmallHom W₁ X₁ ((shiftFunctor C₁ m).obj Y₁)) → L₁.obj X₁ ⟶ L₁.obj ((shiftFunctor C₁ m).obj Y₁))
              f))
          (CategoryStruct.comp (Y := G.obj (Functor.obj.{v₁', v₁', u₁', u₁'} (shiftFunctor D₁ m) (L₁.obj Y₁)))
            (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso L₁ m)) Y₁))
            (CategoryStruct.comp (Y := Functor.obj.{v₂', v₂', u₂', u₂'} (shiftFunctor D₂ m) (G.obj (L₁.obj Y₁)))
              (NatTrans.app (Iso.hom (Functor.commShiftIso G m)) (L₁.obj Y₁))
              (Functor.map (shiftFunctor D₂ m) (e.inv.app Y₁) ≫
                CategoryStruct.comp (Y :=
                  L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
                  (NatTrans.app (Iso.inv (Functor.commShiftIso L₂ m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁))
                  (L₂.map
                      (CategoryStruct.comp (Y :=
                        Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁))
                        (NatTrans.app (Iso.inv (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁)
                        (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁)) ≫
                    L₂.map (Functor.map (shiftFunctor C₂ m) eY.hom))))))
    (L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        CategoryStruct.comp (Y := G.obj (L₁.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
          (G.map
            ((SmallHom.equiv W₁ L₁ :
                (a : SmallHom W₁ X₁ ((shiftFunctor C₁ m).obj Y₁)) → L₁.obj X₁ ⟶ L₁.obj ((shiftFunctor C₁ m).obj Y₁))
              f))
          (CategoryStruct.comp (Y := G.obj (Functor.obj.{v₁', v₁', u₁', u₁'} (shiftFunctor D₁ m) (L₁.obj Y₁)))
            (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso L₁ m)) Y₁))
            (CategoryStruct.comp (Y := Functor.obj.{v₂', v₂', u₂', u₂'} (shiftFunctor D₂ m) (G.obj (L₁.obj Y₁)))
              (NatTrans.app (Iso.hom (Functor.commShiftIso G m)) (L₁.obj Y₁))
              (Functor.map (shiftFunctor D₂ m) (e.inv.app Y₁) ≫
                NatTrans.app (Iso.inv (Functor.commShiftIso L₂ m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
                  L₂.map (Functor.map (shiftFunctor C₂ m) eY.hom)))))
⊢ Eq (α := L₂.obj X₂ ⟶ L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) Y₂))
    (L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        CategoryStruct.comp (Y := G.obj (L₁.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
          (G.map
            ((SmallHom.equiv W₁ L₁ :
                (a : SmallHom W₁ X₁ ((shiftFunctor C₁ m).obj Y₁)) → L₁.obj X₁ ⟶ L₁.obj ((shiftFunctor C₁ m).obj Y₁))
              f))
          (CategoryStruct.comp (Y := G.obj (Functor.obj.{v₁', v₁', u₁', u₁'} (shiftFunctor D₁ m) (L₁.obj Y₁)))
            (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso L₁ m)) Y₁))
            (CategoryStruct.comp (Y := Functor.obj.{v₂', v₂', u₂', u₂'} (shiftFunctor D₂ m) (G.obj (L₁.obj Y₁)))
              (NatTrans.app (Iso.hom (Functor.commShiftIso G m)) (L₁.obj Y₁))
              (Functor.map (shiftFunctor D₂ m) (e.inv.app Y₁) ≫
                CategoryStruct.comp (Y :=
                  L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
                  (NatTrans.app (Iso.inv (Functor.commShiftIso L₂ m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁))
                  (CategoryStruct.comp (Y :=
                    L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
                    (L₂.map (NatTrans.app (Iso.inv (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
                    (L₂.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁) ≫
                      L₂.map (Functor.map (shiftFunctor C₂ m) eY.hom)))))))
    (L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        CategoryStruct.comp (Y := G.obj (L₁.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
          (G.map
            ((SmallHom.equiv W₁ L₁ :
                (a : SmallHom W₁ X₁ ((shiftFunctor C₁ m).obj Y₁)) → L₁.obj X₁ ⟶ L₁.obj ((shiftFunctor C₁ m).obj Y₁))
              f))
          (CategoryStruct.comp (Y := G.obj (Functor.obj.{v₁', v₁', u₁', u₁'} (shiftFunctor D₁ m) (L₁.obj Y₁)))
            (G.map (NatTrans.app (Iso.hom (Functor.commShiftIso L₁ m)) Y₁))
            (CategoryStruct.comp (Y := Functor.obj.{v₂', v₂', u₂', u₂'} (shiftFunctor D₂ m) (G.obj (L₁.obj Y₁)))
              (NatTrans.app (Iso.hom (Functor.commShiftIso G m)) (L₁.obj Y₁))
              (Functor.map (shiftFunctor D₂ m) (e.inv.app Y₁) ≫
                NatTrans.app (Iso.inv (Functor.commShiftIso L₂ m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
                  L₂.map (Functor.map (shiftFunctor C₂ m) eY.hom)))))

Tactic:
nth_rw 2 [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc