Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: 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₁

pp: 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₂

pp: 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₃

Tactic:
· dsimp
      simp only [← Functor.map_comp]
      congr 1
      cat_disch

Goal state after:
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₃