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₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝⁹ : AddMonoid M
inst✝⁸ : HasShift C₁ M
inst✝⁷ : HasShift C₂ 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₂
inst✝¹ : W₁.IsCompatibleWithShift M
inst✝ : W₂.IsCompatibleWithShift M
m : M
f : ShiftedHom X₁ Y₁ m
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ W₂.Q.map eX.inv ≫
      e.hom.app X₁ ≫
        (Φ.localizedFunctor W₁.Q W₂.Q).map (W₁.Q.map f) ≫
          (Φ.localizedFunctor W₁.Q W₂.Q).map
              ((Functor.commShiftIso W₁.Q m).hom.app Y₁ ≫ (Functor.commShiftIso W₁.Q m).inv.app Y₁) ≫
            e.inv.app ((shiftFunctor C₁ m).obj Y₁) ≫
              W₂.Q.map ((Functor.commShiftIso Φ.functor m).hom.app Y₁) ≫
                (Functor.commShiftIso W₂.Q m).hom.app (Φ.functor.obj Y₁) ≫
                  (shiftFunctor W₂.Localization m).map (W₂.Q.map eY.hom) =
    W₂.Q.map eX.inv ≫
      W₂.Q.map (Φ.functor.map f) ≫
        W₂.Q.map ((Functor.commShiftIso Φ.functor m).hom.app Y₁) ≫
          (Functor.commShiftIso W₂.Q m).hom.app (Φ.functor.obj Y₁) ≫
            (shiftFunctor W₂.Localization m).map (W₂.Q.map eY.hom)

Tactic:
]

Goal state after:
C₁ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝⁹ : AddMonoid M
inst✝⁸ : HasShift C₁ M
inst✝⁷ : HasShift C₂ 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₂
inst✝¹ : W₁.IsCompatibleWithShift M
inst✝ : W₂.IsCompatibleWithShift M
m : M
f : ShiftedHom X₁ Y₁ m
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ W₂.Q.map eX.inv ≫
      e.hom.app X₁ ≫
        (Φ.localizedFunctor W₁.Q W₂.Q).map (W₁.Q.map f) ≫
          (Φ.localizedFunctor W₁.Q W₂.Q).map
              ((Functor.commShiftIso W₁.Q m).hom.app Y₁ ≫ (Functor.commShiftIso W₁.Q m).inv.app Y₁) ≫
            e.inv.app ((shiftFunctor C₁ m).obj Y₁) ≫
              W₂.Q.map ((Functor.commShiftIso Φ.functor m).hom.app Y₁) ≫
                (Functor.commShiftIso W₂.Q m).hom.app (Φ.functor.obj Y₁) ≫
                  (shiftFunctor W₂.Localization m).map (W₂.Q.map eY.hom) =
    W₂.Q.map eX.inv ≫
      W₂.Q.map (Φ.functor.map f) ≫
        W₂.Q.map ((Functor.commShiftIso Φ.functor m).hom.app Y₁) ≫
          (Functor.commShiftIso W₂.Q m).hom.app (Φ.functor.obj Y₁) ≫
            (shiftFunctor W₂.Localization m).map (W₂.Q.map eY.hom)