-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
this :
  Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
        CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯)))))
          (X.ω₁.map (homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯))
          (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂)) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₁.map (homOfLE ⋯))))))
          (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁))
          (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
simp :
  ∀
    (this :
      Eq (α :=
        X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
        (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯)))))
            (X.ω₁.map
              ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
                homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯))
            (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂)) :
          X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
        (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
            CategoryStruct.comp (Y :=
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (X.ω₁.obj (mk₁ (F.map (D₁.map (homOfLE ⋯))))))
              (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁))
              (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))) :
          X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
              (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))),
    Eq (α :=
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
      (X.ω₁.map
          (Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 1) (f.app 2) ⋯) ≫
            (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom) ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
          Functor.map (shiftFunctor C (A := ℤ) 1)
            (X.ω₁.map
              ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
                Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
                  (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom)))
⊢ Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    ((X.ω₁.map (Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 1) (f.app 2) ⋯)) ≫
        X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom ≫
          X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂) ≫
            Functor.map (shiftFunctor C (A := ℤ) 1)
              (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).inv)) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          (X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯))))))
        (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
          X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
            Functor.map (shiftFunctor C (A := ℤ) 1)
              (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv))
        (Functor.map (shiftFunctor C (A := ℤ) 1)
          (X.ω₁.map (Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 0) (f.app 1) ⋯)))) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (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 ⊢

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp