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 : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        ((mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app (mk₂ f g)))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        ((mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app (mk₂ f g)))
      ({
            app := fun D ↦
              X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                X.δ'.app ((F.mapComposableArrows 2).obj D) ≫
                  (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
            naturality := ⋯ }.app
        (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 _))) ?_ ?_ ?_

Goal state after:
case refine_1
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 : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            ((mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            ((mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app (mk₂ f g)))
          ({
                app := fun D ↦
                  X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                    X.δ'.app ((F.mapComposableArrows 2).obj D) ≫
                      (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
                naturality := ⋯ }.app
            (mk₂ f g))).mor₁ ≫
      (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 0 homMk₁._proof_4))
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 1 homMk₁._proof_5))
            ⋯)).hom =
    (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 1 2 ⋯ ⋯).obj (mk₂ f g))).obj' 0 homMk₁._proof_4))
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 1 2 ⋯ ⋯).obj (mk₂ f g))).obj' 1 homMk₁._proof_5))
            ⋯)).hom ≫
      (X.triangle (F.map f) (F.map g)).mor₁

case refine_2
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 : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            ((mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            ((mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app (mk₂ f g)))
          ({
                app := fun D ↦
                  X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                    X.δ'.app ((F.mapComposableArrows 2).obj D) ≫
                      (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
                naturality := ⋯ }.app
            (mk₂ f g))).mor₂ ≫
      (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 1 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 0 homMk₁._proof_4))
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 1 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 1 homMk₁._proof_5))
            ⋯)).hom =
    (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 0 homMk₁._proof_4))
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 1 homMk₁._proof_5))
            ⋯)).hom ≫
      (X.triangle (F.map f) (F.map g)).mor₂

case refine_3
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 : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ (Triangle.mk
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            ((mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app (mk₂ f g)))
          ((F.mapComposableArrows 1 ⋙ X.ω₁).map
            ((mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app (mk₂ f g)))
          ({
                app := fun D ↦
                  X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                    X.δ'.app ((F.mapComposableArrows 2).obj D) ≫
                      (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
                naturality := ⋯ }.app
            (mk₂ f g))).mor₃ ≫
      (shiftFunctor C 1).map
        (X.ω₁.mapIso
            (isoMk₁
              (Iso.refl
                (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 1 2 ⋯ ⋯).obj (mk₂ f g))).obj' 0 homMk₁._proof_4))
              (Iso.refl
                (((F.mapComposableArrows 1).obj ((functorArrows ι' 0 1 2 ⋯ ⋯).obj (mk₂ f g))).obj' 1 homMk₁._proof_5))
              ⋯)).hom =
    (X.ω₁.mapIso
          (isoMk₁
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 1 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 0 homMk₁._proof_4))
            (Iso.refl
              (((F.mapComposableArrows 1).obj ((functorArrows ι' 1 2 2 ⋯ ⋯).obj (mk₂ f g))).obj' 1 homMk₁._proof_5))
            ⋯)).hom ≫
      (X.triangle (F.map f) (F.map g)).mor₃