awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X

Tactic:
have eq' : t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncGELTToLTGE a b).app X :=
      t.to_truncLT_obj_ext
        (by dsimp; exact t.from_truncGE_obj_ext (by simpa using H.comm₁))
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
pos : IsIso (t.liftTruncLT m₁ (b - 1) b ⋯)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
rw [← eq']
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ b - 1 + 1 = b

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLT b).map m₁ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
simp [truncGELT]

Premises used: CategoryTheory.Triangulated.TStructure.truncGELT
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncLT b).map m₁

Tactic:
have fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫
        t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncLT b).map m₁ :=
      t.to_truncLT_obj_ext (by simp [truncGELT])
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncLT b).map m₁
⊢ IsIso (t.liftTruncLT m₁ (b - 1) b ⋯)

Tactic:
IsIso.of_isIso_fac_left fac

Premises used: CategoryTheory.IsIso.of_isIso_fac_left
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncLT b).map m₁
⊢ IsIso (t.liftTruncLT m₁ (b - 1) b ⋯)

Tactic:
exact IsIso.of_isIso_fac_left fac

Premises used: CategoryTheory.IsIso.of_isIso_fac_left
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : ¬a ≤ b
⊢ b < a

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
⟨0, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
neg : (t.truncGELTToLTGE a b).app X ≫ 0 = 𝟙 ((t.truncGELT a b).obj X)
neg₁ : 0 ≫ (t.truncGELTToLTGE a b).app X = 𝟙 ((t.truncLTGE a b).obj X)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
refine ⟨0, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
⊢ b - 1 < a

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
⊢ (t.truncGELTToLTGE a b).app X ≫ 0 = 𝟙 ((t.truncGELT a b).obj X)

Tactic:
exact IsZero.eq_of_src (t.isZero _ (b-1) a (by lia)) _ _

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isZero, CategoryTheory.Limits.IsZero.eq_of_src, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
⊢ 0 ≫ (t.truncGELTToLTGE a b).app X = 𝟙 ((t.truncLTGE a b).obj X)

Tactic:
exact IsZero.eq_of_src (t.isZero _ (b-1) a (by lia)) _ _

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isZero, CategoryTheory.Limits.IsZero.eq_of_src, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
rw : IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X)
⊢ IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))

Tactic:
rw [← t.truncLT_map_truncGE_map_truncLTι_app_fac a b X]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
n : ℤ
X Y : Triangle.{v, u} C
f : X ⟶ Y
⊢ HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₁ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₂)
        n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) X.mor₁) ≫
      Functor.map (CategoryTheory.shiftFunctor C n) f.hom₂ =
    Functor.map (CategoryTheory.shiftFunctor C n) f.hom₁ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₁ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₂)
        n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₁)

Tactic:
simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₁]

Premises used: CategoryTheory.Linear.units_smul_comp, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
n : ℤ
X Y : Triangle.{v, u} C
f : X ⟶ Y
⊢ HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) X.obj₃)
        n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) X.mor₂) ≫
      Functor.map (CategoryTheory.shiftFunctor C n) f.hom₃ =
    Functor.map (CategoryTheory.shiftFunctor C n) f.hom₂ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C n) Y.obj₃)
        n.negOnePow (Functor.map (CategoryTheory.shiftFunctor C n) Y.mor₂)

Tactic:
simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₂]

Premises used: CategoryTheory.Linear.units_smul_comp, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C 0) T).mor₁ ≫ Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₂) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₁) ≫ (Functor.obj (𝟭 (Triangle.{v, u} C)) T).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C 0) T).mor₂ ≫ Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₃) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₂) ≫ (Functor.obj (𝟭 (Triangle.{v, u} C)) T).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
T : Triangle.{v, u} C
dsimp :
  HSMul.hSMul (α := ℤˣ) (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₁))
        1
        (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 0)) T.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₃ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₁)) ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorZero C ℤ)) T.obj₁) =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorZero C ℤ)) T.obj₃ ≫ T.mor₃
⊢ (Functor.obj (shiftFunctor C 0) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₃) ≫ (Functor.obj (𝟭 (Triangle.{v, u} C)) T).mor₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
T : Triangle.{v, u} C
⊢ HSMul.hSMul (α := ℤˣ) (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₁))
        1
        (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C 1 0)) T.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₃ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
              (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₁)) ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorZero C ℤ)) T.obj₁) =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorZero C ℤ)) T.obj₃ ≫ T.mor₃

Tactic:
simp only [one_smul, assoc, shiftFunctorComm_zero_hom_app,
          ← Functor.map_comp, Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id,
          comp_id, NatTrans.naturality, Functor.id_map]

Premises used: CategoryTheory.shiftFunctorComm_zero_hom_app, CategoryTheory.Category.assoc, CategoryTheory.Functor.id_map, CategoryTheory.Category.comp_id, one_smul, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b n : ℤ
h : a + b = n
T : Triangle.{v, u} C
subst :
  (Functor.obj (shiftFunctor C (a + b)) T).mor₁ ≫
      Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₂) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₁) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₁
⊢ (Functor.obj (shiftFunctor C n) T).mor₁ ≫ Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₂) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₁) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₁

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
dsimp :
  HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂)
        (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₁) ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₁ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂))
        b.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C b)
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₁)))
⊢ (Functor.obj (shiftFunctor C (a + b)) T).mor₁ ≫
      Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₂) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₁) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b n : ℤ
h : a + b = n
T : Triangle.{v, u} C
subst :
  (Functor.obj (shiftFunctor C (a + b)) T).mor₂ ≫
      Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₃) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₂) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₂
⊢ (Functor.obj (shiftFunctor C n) T).mor₂ ≫ Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₃) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₂) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₂

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
dsimp :
  HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃)
        (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₂) ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃ =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂) ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
        b.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C b)
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
⊢ (Functor.obj (shiftFunctor C (a + b)) T).mor₂ ≫
      Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₃) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₂) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b n : ℤ
h : a + b = n
T : Triangle.{v, u} C
subst :
  (Functor.obj (shiftFunctor C (a + b)) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₃) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₃
⊢ (Functor.obj (shiftFunctor C n) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₃) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₃

Tactic:
subst h