awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
zero : T.mor₃ = 0
this_1 : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ fst ≫ T.mor₁ + T.mor₂ ≫ section_ T.mor₂ = 𝟙 T.obj₂

Tactic:
simp only [← hfst, sub_add_cancel]

Premises used: sub_add_cancel
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
zero : T.mor₃ = 0
this_1 : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData.{v, u} T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ T.mor₂ =
    CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃) (Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit))
      biprod.snd

Tactic:
simp [d]
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
zero : T.mor₃ = 0
this_1 : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData.{v, u} T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
refine :
  Eq (α := T.obj₁ ⟶ biprod.{v, u} T.obj₁ T.obj₃) (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit))
    biprod.inl
⊢ ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
refine ⟨biprod.uniqueUpToIso _ _ d.isBilimit, ⟨?_, by simp [d]⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
zero : T.mor₃ = 0
this_1 : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData.{v, u} T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃)
      (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃) biprod.inl biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃)
      (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃) biprod.inl biprod.snd
⊢ Eq (α := T.obj₁ ⟶ biprod.{v, u} T.obj₁ T.obj₃) (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit))
    biprod.inl

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
zero : T.mor₃ = 0
this_1 : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData.{v, u} T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃)
      (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃) biprod.inl biprod.fst

Tactic:
simpa [d] using d.bicone.inl_fst

Premises used: CategoryTheory.Limits.BinaryBicone.inl_fst, CategoryTheory.Limits.BinaryBiproductData.bicone
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
zero : T.mor₃ = 0
this_1 : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData.{v, u} T.obj₁ T.obj₃ := binaryBiproductData T hT zero (section_ T.mor₂) ⋯ fst ⋯
⊢ CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃)
      (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} T.obj₁ T.obj₃) biprod.inl biprod.snd

Tactic:
simpa [d] using d.bicone.inl_snd

Premises used: CategoryTheory.Limits.BinaryBiproductData.bicone, CategoryTheory.Limits.BinaryBicone.inl_snd
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ : C
obtain :
  ∀ (Y : C) (g : X₁ ⟶ Y) (h : Y ⟶ X₂)
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g h 0)),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (binaryBiproductTriangle X₁ X₂)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (binaryBiproductTriangle X₁ X₂)

Tactic:
obtain ⟨Y, g, h, mem⟩ := distinguished_cocone_triangle₂ (0 : X₂ ⟶ X₁⟦(1 : ℤ)⟧)

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g h 0)
obtain :
  ∀
    (e :
      Triangle.obj₂ (Triangle.mk g h 0) ≅
        biprod.{v, u} (Triangle.obj₁ (Triangle.mk g h 0)) (Triangle.obj₃ (Triangle.mk g h 0)))
    (he₁ : Triangle.mor₁ (Triangle.mk g h 0) ≫ e.hom = biprod.inl)
    (he₂ : Triangle.mor₂ (Triangle.mk g h 0) = e.hom ≫ biprod.snd),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (binaryBiproductTriangle X₁ X₂)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (binaryBiproductTriangle X₁ X₂)

Tactic:
obtain ⟨e, ⟨he₁, he₂⟩⟩ := exists_iso_binaryBiproduct_of_distTriang _ mem rfl

Premises used: CategoryTheory.Pretriangulated.exists_iso_binaryBiproduct_of_distTriang, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g h 0)
e :
  Triangle.obj₂ (Triangle.mk g h 0) ≅
    biprod.{v, u} (Triangle.obj₁ (Triangle.mk g h 0)) (Triangle.obj₃ (Triangle.mk g h 0))
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (binaryBiproductTriangle X₁ X₂)

Tactic:
isomorphic_distinguished _ mem _ (Iso.symm ?_)

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g h 0)
e :
  Triangle.obj₂ (Triangle.mk g h 0) ≅
    biprod.{v, u} (Triangle.obj₁ (Triangle.mk g h 0)) (Triangle.obj₃ (Triangle.mk g h 0))
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
refine : Iso (C := Triangle.{v, u} C) (Triangle.mk g h 0) (binaryBiproductTriangle X₁ X₂)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (binaryBiproductTriangle X₁ X₂)

Tactic:
refine isomorphic_distinguished _ mem _ (Iso.symm ?_)

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g h 0)
e :
  Triangle.obj₂ (Triangle.mk g h 0) ≅
    biprod.{v, u} (Triangle.obj₁ (Triangle.mk g h 0)) (Triangle.obj₃ (Triangle.mk g h 0))
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ Triangle.mor₃ (Triangle.mk g h 0) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.refl (Triangle.obj₁ (Triangle.mk g h 0)))) =
    Iso.hom (Iso.refl (Triangle.obj₃ (Triangle.mk g h 0))) ≫ Triangle.mor₃ (binaryBiproductTriangle X₁ X₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g h 0)
e :
  Triangle.obj₂ (Triangle.mk g h 0) ≅
    biprod.{v, u} (Triangle.obj₁ (Triangle.mk g h 0)) (Triangle.obj₃ (Triangle.mk g h 0))
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ Iso (C := Triangle.{v, u} C) (Triangle.mk g h 0) (binaryBiproductTriangle X₁ X₂)

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) e (Iso.refl _)
    (by cat_disch) (by cat_disch) (by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X₁ X₂ : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (binaryProductTriangle X₁ X₂)

Tactic:
isomorphic_distinguished _ (binaryBiproductTriangle_distinguished X₁ X₂) _
    (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂)

Premises used: CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.binaryBiproductTriangle_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
obtain :
  ∀ (Z : C) (f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z)
    (f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
    (hT' :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f₁ f₂ f₃)),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (productTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (productTriangle T)

Tactic:
obtain ⟨Z, f₂, f₃, hT'⟩ := distinguished_cocone_triangle f₁

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
Z : C
f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
hT' :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f₁ f₂ f₃)
T' : Triangle.{v, u} C := Triangle.mk f₁ f₂ f₃
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'

Tactic:
change T' ∈ distTriang C at hT'
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
Z : C
f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
T' : Triangle.{v, u} C := Triangle.mk f₁ f₂ f₃
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
j : J
⊢ T'.mor₁ ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁

Tactic:
simp [f₁, T']
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
Z : C
f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
T' : Triangle.{v, u} C := Triangle.mk f₁ f₂ f₃
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
φ : (j : J) → T' ⟶ T j :=
  fun (j : J) ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun (j : J) ↦ (T j).obj₁) j)
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
⊢ φ'.hom₁ = 𝟙 T'.obj₁

Tactic:
have h₁ : φ'.hom₁ = 𝟙 _ := by cat_disch
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
Z : C
f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
T' : Triangle.{v, u} C := Triangle.mk f₁ f₂ f₃
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
φ : (j : J) → T' ⟶ T j :=
  fun (j : J) ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun (j : J) ↦ (T j).obj₁) j)
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
⊢ φ'.hom₂ = 𝟙 T'.obj₂

Tactic:
have h₂ : φ'.hom₂ = 𝟙 _ := by cat_disch
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
Z : C
f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
T' : Triangle.{v, u} C := Triangle.mk f₁ f₂ f₃
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
φ : (j : J) → T' ⟶ T j :=
  fun (j : J) ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun (j : J) ↦ (T j).obj₁) j)
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
rw : IsIso.{v, u} (𝟙 T'.obj₁)
⊢ IsIso φ'.hom₁

Tactic:
rw [h₁]
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
hT :
  ∀ (j : J), Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (T j)
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_6 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_7 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_8 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
f₁ : Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) :=
  Limits.Pi.map fun (j : J) ↦ (T j).mor₁
Z : C
f₂ : (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁)
T' : Triangle.{v, u} C := Triangle.mk f₁ f₂ f₃
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
φ : (j : J) → T' ⟶ T j :=
  fun (j : J) ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun (j : J) ↦ (T j).obj₁) j)
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
⊢ IsIso.{v, u} (𝟙 T'.obj₁)

Tactic:
infer_instance