awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ (f + g).hom₁ = (g + f).hom₁

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ (f + g).hom₂ = (g + f).hom₂

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ (f + g).hom₃ = (g + f).hom₃

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
R : Type u_1
inst_3 : Semiring R
inst_4 : Linear.{u_1, v, u} R C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : ∀ (n : ℤ), Functor.Linear.{u_1, v, u, v, u} R (shiftFunctor C n)
⊢ ∀ (x y : R) (b : T₁ ⟶ T₂), (x * y) • b = x • y • b

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
R : Type u_1
inst_3 : Semiring R
inst_4 : Linear.{u_1, v, u} R C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : ∀ (n : ℤ), Functor.Linear.{u_1, v, u, v, u} R (shiftFunctor C n)
⊢ ∀ (b : T₁ ⟶ T₂), HSMul.hSMul.{u_1, v, v} (α := R) 1 b = b

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
R : Type u_1
inst_3 : Semiring R
inst_4 : Linear.{u_1, v, u} R C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : ∀ (n : ℤ), Functor.Linear.{u_1, v, u, v, u} R (shiftFunctor C n)
⊢ ∀ (a : R), HSMul.hSMul (β := T₁ ⟶ T₂) a 0 = 0

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
R : Type u_1
inst_3 : Semiring R
inst_4 : Linear.{u_1, v, u} R C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : ∀ (n : ℤ), Functor.Linear.{u_1, v, u, v, u} R (shiftFunctor C n)
⊢ ∀ (a : R) (x y : T₁ ⟶ T₂), a • (x + y) = a • x + a • y

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
R : Type u_1
inst_3 : Semiring R
inst_4 : Linear.{u_1, v, u} R C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : ∀ (n : ℤ), Functor.Linear.{u_1, v, u, v, u} R (shiftFunctor C n)
⊢ ∀ (r s : R) (x : T₁ ⟶ T₂), (r + s) • x = r • x + s • x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
R : Type u_1
inst_3 : Semiring R
inst_4 : Linear.{u_1, v, u} R C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : ∀ (n : ℤ), Functor.Linear.{u_1, v, u, v, u} R (shiftFunctor C n)
⊢ ∀ (x : T₁ ⟶ T₂), HSMul.hSMul.{u_1, v, v} (α := R) 0 x = 0

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
X₁ X₂ : C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasBinaryBiproduct.{v, u} X₁ X₂
⊢ Triangle.mor₂ (binaryProductTriangle X₁ X₂) ≫
      Iso.hom (Iso.refl (Triangle.obj₃.{v, u} (binaryProductTriangle X₁ X₂))) =
    CategoryStruct.comp (Y := Triangle.obj₂.{v, u} (binaryBiproductTriangle X₁ X₂))
      (Iso.hom (Iso.symm (biprod.isoProd X₁ X₂))) (Triangle.mor₂ (binaryBiproductTriangle X₁ X₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
X₁ X₂ : C
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasBinaryBiproduct.{v, u} X₁ X₂
⊢ Triangle.mor₃ (binaryProductTriangle X₁ X₂) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.refl (Triangle.obj₁.{v, u} (binaryProductTriangle X₁ X₂)))) =
    Iso.hom (Iso.refl (Triangle.obj₃.{v, u} (binaryProductTriangle X₁ X₂))) ≫
      Triangle.mor₃ (binaryBiproductTriangle X₁ X₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
T' : Triangle.{v, u} C
φ : (j : J) → T' ⟶ T j
dsimp :
  Eq (α := T'.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
    (T'.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁))
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) (Pi.lift fun (j : J) ↦ (φ j).hom₃)
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))))
⊢ T'.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁) =
    (Pi.lift fun (j : J) ↦ (φ j).hom₃) ≫ (productTriangle T).mor₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
T' : Triangle.{v, u} C
φ : (j : J) → T' ⟶ T j
rw :
  Eq (α := T'.obj₃ ⟶ piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₁)
    (T'.mor₃ ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁))
        (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) (Pi.lift fun (j : J) ↦ (φ j).hom₃)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₃))
⊢ Eq (α := T'.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
    (T'.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁))
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) (Pi.lift fun (j : J) ↦ (φ j).hom₃)
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))))

Tactic:
rw [← cancel_mono (piComparison _ _), assoc, assoc, assoc, IsIso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.piComparison, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
h₁ : m.hom₁ = TriangleMorphism.hom₁ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
h₂ : m.hom₂ = TriangleMorphism.hom₂ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
h₃ : m.hom₃ = TriangleMorphism.hom₃ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
⊢ m = (fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
j : J
⊢ m.hom₁ ≫ Pi.π (fun (j : J) ↦ (T j).obj₁) j =
    CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
      (TriangleMorphism.hom₁ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s) :
        s.pt.obj₁ ⟶ (fan T).pt.obj₁)
      (Pi.π (fun (j : J) ↦ (T j).obj₁) j)

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m.hom₁ = TriangleMorphism.hom₁ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)

Tactic:
exact Pi.hom_ext _ _ (fun j => (by simp [← hm]))

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
j : J
⊢ m.hom₂ ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j =
    CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂)
      (TriangleMorphism.hom₂ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s) :
        s.pt.obj₂ ⟶ (fan T).pt.obj₂)
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j)

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m.hom₂ = TriangleMorphism.hom₂ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)

Tactic:
exact Pi.hom_ext _ _ (fun j => (by simp [← hm]))

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
j : J
⊢ m.hom₃ ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j =
    CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃)
      (TriangleMorphism.hom₃ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s) :
        s.pt.obj₃ ⟶ (fan T).pt.obj₃)
      (Pi.π (fun (j : J) ↦ (T j).obj₃) j)

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m.hom₃ = TriangleMorphism.hom₃ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)

Tactic:
exact Pi.hom_ext _ _ (fun j => (by simp [← hm]))

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
⊢ HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂

Tactic:
have : HasProduct (fun j => (T j).obj₂⟦(1 : ℤ)⟧) :=
    ⟨_, isLimitFanMkObjOfIsLimit (shiftFunctor C (1 : ℤ)) _ _
      (productIsProduct (fun j => (T j).obj₂))⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
dsimp :
  Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Limits.Pi.map fun (j : J) ↦ (T j).mor₁)))
    0
⊢ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (productTriangle T).mor₁ = 0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
change :
  Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁)))
    0
⊢ Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Limits.Pi.map fun (j : J) ↦ (T j).mor₁)))
    0

Tactic:
change _ ≫ (Pi.lift (fun j => Pi.π _ j ≫ (T j).mor₁))⟦(1 : ℤ)⟧' = 0

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Limits.Pi.π, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Pi.lift, CategoryTheory.Pretriangulated.Triangle.mor₁, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
rw :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃)
      (piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂))
    (CategoryStruct.comp (Y :=
      piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
          (Functor.map (shiftFunctor C (A := ℤ) 1)
            (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁))
          (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₂))))
    0
⊢ Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁)))
    0

Tactic:
rw [assoc, ← cancel_mono (piComparison _ _), zero_comp, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.piComparison, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
j : J
⊢ Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂)
    (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂)
        (CategoryStruct.comp (Y :=
          piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
          (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
          (CategoryStruct.comp (Y :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
            (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
            (CategoryStruct.comp (Y :=
              Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
              (Functor.map (shiftFunctor C (A := ℤ) 1)
                (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁))
              (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₂))))
        (Pi.π (fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂) j) :
      (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂)
    (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂) 0
        (Pi.π (fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂) j) :
      (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂)

Tactic:
simp [h j]