Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.ω₁.map (homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫ X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (X.ω₁.map ((F.mapComposableArrows 1).map (homMk₁ (f.app 1) (f.app 2) ⋯)) ≫
        X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom ≫
          X.δ'.app ((F.mapComposableArrows 2).obj D₂) ≫
            (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).inv)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom) =
    ((X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
          X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
            (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv)) ≫
        (shiftFunctor C 1).map (X.ω₁.map ((F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯)))) ≫
      (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom)

Tactic:
simp only [← Functor.map_comp_assoc, ← Functor.map_comp, Category.assoc,
      Iso.inv_hom_id, Functor.map_id, Category.comp_id] at this ⊢

Goal state after:
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ X.ω₁.map
        ((F.mapComposableArrows 1).map (homMk₁ (f.app 1) (f.app 2) ⋯) ≫
          (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map
          (X.ω₁.map
            ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
              (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
                (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom))