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₁ Z₁ : C₁
X₂ Y₂ Z₂ : 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₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : 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₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ (ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eX.inv ≫ e.hom.app X₁)).comp
      (((((SmallShiftedHom.equiv W₁ W₁.Q) f).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
            (((SmallShiftedHom.equiv W₁ W₁.Q) g).map (Φ.localizedFunctor W₁.Q W₂.Q)) h).comp
        (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) ⋯)
      ⋯ =
    ((ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eX.inv ≫ e.hom.app X₁)).comp
          ((((SmallShiftedHom.equiv W₁ W₁.Q) f).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
            (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ W₂.Q.map eY.hom)) ⋯)
          ⋯).comp
      ((ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eY.inv ≫ e.hom.app Y₁)).comp
        ((((SmallShiftedHom.equiv W₁ W₁.Q) g).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
          (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) ⋯)
        ⋯)
      h

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₀]

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₁ Z₁ : C₁
X₂ Y₂ Z₂ : 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₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : 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₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ (ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eX.inv ≫ e.hom.app X₁)).comp
      ((((SmallShiftedHom.equiv W₁ W₁.Q) f).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
        ((((SmallShiftedHom.equiv W₁ W₁.Q) g).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
          (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ (W₂.Q.map eX.inv ≫ e.hom.app X₁)).comp
      ((((SmallShiftedHom.equiv W₁ W₁.Q) f).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
        ((ShiftedHom.mk₀ 0 ⋯ ((e.inv.app Y₁ ≫ W₂.Q.map eY.hom) ≫ W₂.Q.map eY.inv ≫ e.hom.app Y₁)).comp
          ((((SmallShiftedHom.equiv W₁ W₁.Q) g).map (Φ.localizedFunctor W₁.Q W₂.Q)).comp
            (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Z₁ ≫ W₂.Q.map eZ.hom)) ⋯)
          ⋯)
        ⋯)
      ⋯