Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁸ : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst✝¹⁷ : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst✝¹⁶ : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝¹⁵ : L₁.IsLocalization W₁
inst✝¹⁴ : L₂.IsLocalization W₂
M : Type w'
inst✝¹³ : AddMonoid M
inst✝¹² : HasShift C₁ M
inst✝¹¹ : HasShift C₂ M
inst✝¹⁰ : HasShift D₁ M
inst✝⁹ : HasShift D₂ M
inst✝⁸ : L₁.CommShift M
inst✝⁷ : L₂.CommShift M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
G : D₁ ⥤ D₂
inst✝¹ : G.CommShift M
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
inst✝ : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
this : HasSmallLocalizedHom W₂ X₂ X₂
⊢ L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        G.map ((SmallHom.equiv W₁ L₁) f) ≫
          e.inv.app ((shiftFunctor C₁ m).obj Y₁) ≫
            L₂.map ((Functor.commShiftIso Φ.functor m).app Y₁ ≪≫ (shiftFunctor C₂ m).mapIso eY).hom =
    (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁)).comp
        ((ShiftedHom.map ((SmallHom.equiv W₁ L₁) f ≫ (Functor.commShiftIso L₁ m).hom.app Y₁) G).comp
          (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯)
        ⋯ ≫
      (Functor.commShiftIso L₂ m).inv.app Y₂

Tactic:
simp only [Functor.comp_obj, NatTrans.app_shift,
    Functor.commShiftIso_comp_hom_app, Functor.commShiftIso_comp_inv_app, assoc,
    Iso.trans_hom, Iso.app_hom, Functor.mapIso_hom, Functor.map_comp, ShiftedHom.map,
    ShiftedHom.comp_mk₀, ShiftedHom.mk₀_comp,
    Functor.commShiftIso_inv_naturality]

Goal state after:
C₁ : Type u₁
inst✝¹⁹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁸ : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst✝¹⁷ : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst✝¹⁶ : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝¹⁵ : L₁.IsLocalization W₁
inst✝¹⁴ : L₂.IsLocalization W₂
M : Type w'
inst✝¹³ : AddMonoid M
inst✝¹² : HasShift C₁ M
inst✝¹¹ : HasShift C₂ M
inst✝¹⁰ : HasShift D₁ M
inst✝⁹ : HasShift D₂ M
inst✝⁸ : L₁.CommShift M
inst✝⁷ : L₂.CommShift M
inst✝⁶ : Φ.functor.CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝² : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
G : D₁ ⥤ D₂
inst✝¹ : G.CommShift M
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
inst✝ : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
this : HasSmallLocalizedHom W₂ X₂ X₂
⊢ L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        G.map ((SmallHom.equiv W₁ L₁) f) ≫
          G.map ((Functor.commShiftIso L₁ m).hom.app Y₁) ≫
            (Functor.commShiftIso G m).hom.app (L₁.obj Y₁) ≫
              (shiftFunctor D₂ m).map (e.inv.app Y₁) ≫
                (Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj Y₁) ≫
                  L₂.map ((Functor.commShiftIso Φ.functor m).inv.app Y₁) ≫
                    L₂.map ((Functor.commShiftIso Φ.functor m).hom.app Y₁) ≫ L₂.map ((shiftFunctor C₂ m).map eY.hom) =
    L₂.map eX.inv ≫
      e.hom.app X₁ ≫
        G.map ((SmallHom.equiv W₁ L₁) f) ≫
          G.map ((Functor.commShiftIso L₁ m).hom.app Y₁) ≫
            (Functor.commShiftIso G m).hom.app (L₁.obj Y₁) ≫
              (shiftFunctor D₂ m).map (e.inv.app Y₁) ≫
                (Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj Y₁) ≫ L₂.map ((shiftFunctor C₂ m).map eY.hom)