awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} 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
w :
  Eq (α :=
    (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
    (CategoryStruct.comp (Y := (t.eTruncGE.obj b').obj ((t.eTruncLT.obj c).obj x))
          (NatTrans.app (t.eTruncGE.map (φ.app 1)) ((t.eTruncLT.obj c).obj x))
          ((t.eTruncGE.obj b').map (NatTrans.app (t.eTruncLT.map (φ.app 2)) x)) ≫
        (t.ω₁δ a' b' c' hab' hbc').app x :
      (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
    ((t.ω₁δ a b c hab hbc).app x ≫
        Functor.map (shiftFunctor C (A := ℤ) 1)
          (CategoryStruct.comp (Y := (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj x))
            (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj x))
            ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) x))) :
      (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
⊢ NatTrans.app (t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) ⋯) ≫ t.ω₁δ a' b' c' hab' hbc') x =
    NatTrans.app
      (t.ω₁δ a b c hab hbc ≫ Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C (A := ℤ) 1))
      x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} 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
⊢ ∀ (X : C),
    Eq (α :=
      (t.eTruncLT.obj ((mk₁ (homOfLE hab)).obj 1)).obj ((t.eTruncGE.obj a).obj X) ⟶
        (t.eTruncLT.obj b' ⋙ t.eTruncGE.obj a').obj X)
      (CategoryStruct.comp (Y := (t.eTruncLT.obj ((mk₁ (homOfLE hab')).obj 1)).obj ((t.eTruncGE.obj a).obj X))
        (NatTrans.app (t.eTruncLT.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 1)) ((t.eTruncGE.obj a).obj X))
        ((t.eTruncLT.obj b').map (NatTrans.app (t.eTruncGE.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 0)) X) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X))
      ((t.eTruncLTGEIsoGELT a b).hom.app X ≫
        CategoryStruct.comp (Y := (t.eTruncGE.obj ((mk₁ (homOfLE hab')).obj 0)).obj ((t.eTruncLT.obj b).obj X))
          (NatTrans.app (t.eTruncGE.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 0)) ((t.eTruncLT.obj b).obj X) :
            (t.eTruncGE.obj ((mk₁ (homOfLE hab)).obj 0)).obj ((t.eTruncLT.obj b).obj X) ⟶
              (t.eTruncGE.obj ((mk₁ (homOfLE hab')).obj 0)).obj ((t.eTruncLT.obj b).obj X))
          ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (NatTrans.app (homMk₁ (φ.app 0) (φ.app 1) ⋯) 1)) X) :
            (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj X) ⟶
              (t.eTruncGE.obj a').obj ((t.eTruncLT.obj ((mk₁ (homOfLE hab')).obj 1)).obj X)))

Tactic:
have h₁ := t.eTruncLTGEIsoGELT_naturality_app a b hab a' b' hab' (homMk₁ (φ.app 0) (φ.app 1))
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_1 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) =
    ((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₁
refine_2 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
      Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) =
    Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₂
refine_3 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        ((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 =
    Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₃
⊢ (t.triangleω₁δ a b c hab hbc).obj X ≅ (t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)

Tactic:
refine Triangle.isoMk _ _ ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
    (t.eTruncLTGEIsoGELT a b).symm.app _) (Iso.refl _) ((t.eTruncGEIsoGEGE a b hab).app _) ?_ ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Iso.trans
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_1 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ 𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) =
    ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
        (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X)) ≫
      (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) =
    ((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₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_1 :
  (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
      (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
        (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ 𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) =
    ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
        (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X)) ≫
      (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
simp only [triangleω₁δ_obj_mor₁, homOfLE_leOfHom, Category.comp_id, Category.assoc]

Premises used: CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.homOfLE_leOfHom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_1 :
  Eq (α :=
    (t.eTruncGE.obj a ⋙ t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj X) ⟶
      (t.eTruncGE.obj a).obj ((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ι b).app ((t.eTruncLT.obj c).obj X)))
    ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)))
⊢ (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
      (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
        (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
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]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map, CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT, CategoryTheory.Triangulated.TStructure.eTruncLT, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ Eq (α :=
    (t.eTruncGE.obj a ⋙ t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj X) ⟶
      (t.eTruncGE.obj a).obj ((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ι b).app ((t.eTruncLT.obj c).obj X)))
    ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_2 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫ (t.eTruncGEToGEGE a b).app ((t.eTruncLT.obj c).obj X) =
    𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) ≫
      (t.eTruncGEπ b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
      Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) =
    Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫ (t.eTruncGEToGEGE a b).app ((t.eTruncLT.obj c).obj X) =
    𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) ≫
      (t.eTruncGEπ b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
simp only [triangleω₁δ_obj_mor₂, eTruncGEToGEGE_app, Category.id_comp,
      ← t.eTruncGEπ_app_eTruncGE_map_app (homOfLE hab), ← NatTrans.naturality,
      eTruncGE_obj_map_eTruncGEπ_app]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app, CategoryTheory.NatTrans.naturality, CategoryTheory.homOfLE, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂, CategoryTheory.Category.id_comp, CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        ((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 =
    Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₃

Tactic:
simp [← Functor.map_comp_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleω₁δ a b c hab hbc).obj X)

Tactic:
isomorphic_distinguished _ (t.eTriangleLTGE_distinguished b _) _
    (t.triangleω₁δObjIso a b c hab hbc X)

Premises used: CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguished, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.TStructure.triangleω₁δObjIso
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
D D' : ComposableArrows EInt 2
φ : D ⟶ D'
obtain :
  ∀ (a b c : EInt) (f : a ⟶ b) (g : b ⟶ c) (φ : mk₂ f g ⟶ D'),
    (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
              t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
          φ ≫
        (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
      (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
        (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
              (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
          φ
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ

Tactic:
obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
D' : ComposableArrows EInt 2
a b c : EInt
f : a ⟶ b
g : b ⟶ c
φ : mk₂ f g ⟶ D'
obtain :
  ∀ (a' b' c' : EInt) (f' : a' ⟶ b') (g' : b' ⟶ c') (φ : mk₂ f g ⟶ mk₂ f' g'),
    (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
              t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
          φ ≫
        (t.ω₁δ ((mk₂ f' g').obj 0) ((mk₂ f' g').obj 1) ((mk₂ f' g').obj 2) ⋯ ⋯).app X =
      (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
        (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
              (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
          φ
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ

Tactic:
obtain ⟨a', b', c', f', g', rfl⟩ := mk₂_surjective D'

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
a' b' c' : EInt
f' : a' ⟶ b'
g' : b' ⟶ c'
φ : mk₂ f g ⟶ mk₂ f' g'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ ((mk₂ f' g').obj 0) ((mk₂ f' g').obj 1) ((mk₂ f' g').obj 2) ⋯ ⋯).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ

Tactic:
NatTrans.congr_app (t.ω₁δ_naturality a b c (leOfHom f) (leOfHom g)
      a' b' c' (leOfHom f') (leOfHom g') φ) X

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, Fin.ofNat, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.NatTrans.congr_app, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
a' b' c' : EInt
f' : a' ⟶ b'
g' : b' ⟶ c'
φ : mk₂ f g ⟶ mk₂ f' g'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ ((mk₂ f' g').obj 0) ((mk₂ f' g').obj 1) ((mk₂ f' g').obj 2) ⋯ ⋯).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ

Tactic:
exact NatTrans.congr_app (t.ω₁δ_naturality a b c (leOfHom f) (leOfHom g)
      a' b' c' (leOfHom f') (leOfHom g') φ) X

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
D : ComposableArrows EInt 2
obtain :
  ∀ (a b c : EInt) (f : a ⟶ b) (g : b ⟶ c),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk
        ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
          (NatTrans.app
            (mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
              SpectralObject._proof_2 SpectralObject._proof_4)
            (mk₂ f g)))
        ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
          (NatTrans.app
            (mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
              SpectralObject._proof_4 SpectralObject._proof_4)
            (mk₂ f g)))
        (NatTrans.app
          { app := fun (D : ComposableArrows EInt 2) ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X,
            naturality := ⋯ }
          (mk₂ f g)))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
            SpectralObject._proof_2 SpectralObject._proof_4)
          D))
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
            SpectralObject._proof_4 SpectralObject._proof_4)
          D))
      (NatTrans.app
        { app := fun (D : ComposableArrows EInt 2) ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }
        D))

Tactic:
obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective