Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case e_a
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
x✝ : C
h₁ :
  ∀ (X : C),
    (t.eTruncLT.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 1)).app ((t.eTruncGE.obj a).obj X) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGE.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 0)).app X) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X =
      (t.eTruncLTGEIsoGELT a b).hom.app X ≫
        (t.eTruncGE.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 0)).app ((t.eTruncLT.obj b).obj X) ≫
          (t.eTruncGE.obj a').map ((t.eTruncLT.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 1)).app X)
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncLT.obj c).obj x✝) ≫
      (t.eTruncLT.obj b').map ((t.eTruncLT.map (φ.app 2)).app x✝) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGEπ a').app ((t.eTruncLT.obj c').obj x✝)) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app ((t.eTruncLT.obj c').obj x✝) ≫
            (t.eTruncGE.obj a').map ((t.eTruncLT.obj b').map ((t.eTruncLTι c').app x✝)) =
    (t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj x✝)) ≫
      (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj x✝) ≫
        (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x✝)) ≫
          (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncLT.obj c).obj x✝)) ≫
            (t.eTruncGE.obj a').map ((t.eTruncLT.obj b').map ((t.eTruncLTι c).app x✝))

Tactic:
rw [← reassoc_of% dsimp% h₁, ← eTruncLTGEIsoGELT_hom_naturality,
    ← eTruncLTGEIsoGELT_hom_naturality, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 2)]

Goal state after:
case e_a
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
x✝ : C
h₁ :
  ∀ (X : C),
    (t.eTruncLT.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 1)).app ((t.eTruncGE.obj a).obj X) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGE.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 0)).app X) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X =
      (t.eTruncLTGEIsoGELT a b).hom.app X ≫
        (t.eTruncGE.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 0)).app ((t.eTruncLT.obj b).obj X) ≫
          (t.eTruncGE.obj a').map ((t.eTruncLT.map ((homMk₁ (φ.app 0) (φ.app 1) ⋯).app 1)).app X)
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncLT.obj c).obj x✝) ≫
      (t.eTruncLT.obj b').map ((t.eTruncLT.map (φ.app 2)).app x✝) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGEπ a').app ((t.eTruncLT.obj c').obj x✝)) ≫
          (t.eTruncLT.obj b').map ((t.eTruncGE.obj a').map ((t.eTruncLTι c').app x✝)) ≫
            (t.eTruncLTGEIsoGELT a' b').hom.app x✝ =
    (t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj x✝)) ≫
      (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj x✝)) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj c).obj x✝)) ≫
          (t.eTruncLT.obj b').map
              ((t.eTruncGE.obj a').map
                ((t.eTruncLT.map (φ.app 2)).app x✝ ≫
                  (t.eTruncLTι ((mk₂ (homOfLE hab') (homOfLE hbc')).obj 2)).app x✝)) ≫
            (t.eTruncLTGEIsoGELT a' b').hom.app x✝