Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case refine_1
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
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂).hom =
    ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
          (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₁

pp: case refine_2
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
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
      ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)).hom =
    (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₂

pp: case refine_3
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
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₃ ≫
      (shiftFunctor C 1).map
        ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
            (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom =
    ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₃

Tactic:
· dsimp
    simp only [triangleω₁δ_obj_mor₁, homOfLE_leOfHom, Category.comp_id, Category.assoc]
    rw [← cancel_epi ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X)),
      ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp,
      ← cancel_epi ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X)),
      Iso.hom_inv_id_app_assoc, eTruncLTLTIsoLT_hom, eTruncLTLTToLT_app,
      ← Functor.map_comp, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app]
    simp

Goal state after:
case refine_2
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
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
      ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)).hom =
    (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₂

case refine_3
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
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₃ ≫
      (shiftFunctor C 1).map
        ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
            (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom =
    ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₃