-- 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} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
refine_1 :
  Triangle.mor₁
        (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
          (NatTrans.app
            {
              app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
                X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                  X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                    Functor.map (shiftFunctor C (A := ℤ) 1)
                      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
              naturality := ⋯ :
              NatTrans (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁)
                (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙
                  (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1) }
            (mk₂ f g))) ≫
      (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 2 2 ⋯ ⋯) (mk₂ f g))).obj' 0
                homMk₁._proof_4))
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 2 2 ⋯ ⋯) (mk₂ f g))).obj' 1
                homMk₁._proof_5))
            ⋯)).hom =
    (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 1 2 ⋯ ⋯) (mk₂ f g))).obj' 0
                homMk₁._proof_4))
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 1 2 ⋯ ⋯) (mk₂ f g))).obj' 1
                homMk₁._proof_5))
            ⋯)).hom ≫
      (X.triangle (F.map f) (F.map g)).mor₁
refine_2 :
  Triangle.mor₂
        (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
          (NatTrans.app
            {
              app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
                X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                  X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                    Functor.map (shiftFunctor C (A := ℤ) 1)
                      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
              naturality := ⋯ :
              NatTrans (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁)
                (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙
                  (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1) }
            (mk₂ f g))) ≫
      (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 1 2 2 ⋯ ⋯) (mk₂ f g))).obj' 0
                homMk₁._proof_4))
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 1 2 2 ⋯ ⋯) (mk₂ f g))).obj' 1
                homMk₁._proof_5))
            ⋯)).hom =
    (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 2 2 ⋯ ⋯) (mk₂ f g))).obj' 0
                homMk₁._proof_4))
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 2 2 ⋯ ⋯) (mk₂ f g))).obj' 1
                homMk₁._proof_5))
            ⋯)).hom ≫
      (X.triangle (F.map f) (F.map g)).mor₂
refine_3 :
  Eq (α :=
    Triangle.obj₃
        (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
          (NatTrans.app
            {
              app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
                X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                  X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                    Functor.map (shiftFunctor C (A := ℤ) 1)
                      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
              naturality := ⋯ :
              NatTrans (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁)
                (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙
                  (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1) }
            (mk₂ f g))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.triangle (F.map f) (F.map g)).obj₁)
    (Triangle.mor₃
        (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
          (NatTrans.app
            {
              app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
                X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                  X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                    Functor.map (shiftFunctor C (A := ℤ) 1)
                      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
              naturality := ⋯ :
              NatTrans (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁)
                (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙
                  (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1) }
            (mk₂ f g))) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (X.ω₁.mapIso
            (isoMk₁
              (Iso.refl
                ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 1 2 ⋯ ⋯) (mk₂ f g))).obj' 0
                  homMk₁._proof_4))
              (Iso.refl
                ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 0 1 2 ⋯ ⋯) (mk₂ f g))).obj' 1
                  homMk₁._proof_5))
              ⋯)).hom)
    ((X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 1 2 2 ⋯ ⋯) (mk₂ f g))).obj' 0
                homMk₁._proof_4))
            (Iso.refl
              ((Functor.obj (F.mapComposableArrows 1) (Functor.obj (functorArrows ι' 1 2 2 ⋯ ⋯) (mk₂ f g))).obj' 1
                homMk₁._proof_5))
            ⋯)).hom ≫
      (X.triangle (F.map f) (F.map g)).mor₃)
⊢ Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
            X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
              X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                Functor.map (shiftFunctor C (A := ℤ) 1)
                  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
          naturality := ⋯ }
        (mk₂ f g)) ≅
    X.triangle (F.map f) (F.map g)

Tactic:
refine Triangle.isoMk _ _ (X.ω₁.mapIso (ComposableArrows.isoMk₁ (Iso.refl _) (Iso.refl _)))
      (X.ω₁.mapIso (ComposableArrows.isoMk₁ (Iso.refl _) (Iso.refl _)))
      (X.ω₁.mapIso (ComposableArrows.isoMk₁ (Iso.refl _) (Iso.refl _))) ?_ ?_ ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.isoMk