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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
x₁ : A ⟶ T.obj₁
hx₁ : x₁ ≫ φ.hom₁ = y₁
refine_2 : x₂ ≫ φ.hom₂ + (x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
refine_2₁ : x₂ ≫ φ.hom₂ + x₁ ≫ T.mor₁ ≫ φ.hom₂ = y₂
refine_2₂ : x₂ ≫ φ.hom₂ + x₁ ≫ φ.hom₁ ≫ T'.mor₁ = y₂
refine_2₃ : x₂ ≫ φ.hom₂ + y₁ ≫ T'.mor₁ = y₂
refine_2₄ : x₂ ≫ φ.hom₂ + (y₂ - x₂ ≫ φ.hom₂) = y₂
refine_2₅ refine_2₆ : y₂ = y₂
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂

Tactic:
rw [add_comp, assoc, φ.comm₁, reassoc_of% hx₁, ← hy₁, add_sub_cancel]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.add_comp, add_sub_cancel, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁
-- 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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
dsimp :
  IsIso (X := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁)
⊢ IsIso (X := (Functor.obj (rotate C) T).obj₃) (TriangleMorphism.hom₃ (Functor.map (rotate C) φ))

Tactic:
dsimp
-- 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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
⊢ IsIso (X := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁)

Tactic:
infer_instance
-- 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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
dsimp :
  IsIso (X := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)
⊢ IsIso (X := (Functor.obj (invRotate C) T).obj₁) (TriangleMorphism.hom₁ (Functor.map (invRotate C) φ))

Tactic:
dsimp
-- 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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso (X := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)

Tactic:
infer_instance
-- 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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
dsimp : IsIso φ.hom₂
⊢ IsIso (X := (Functor.obj (invRotate C) T).obj₃) (TriangleMorphism.hom₃ (Functor.map (invRotate C) φ))

Tactic:
dsimp
-- 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 T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso φ.hom₂

Tactic:
infer_instance
-- 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
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
⊢ Mono T.mor₁

Tactic:
have : Mono T.mor₁ := T.mono₁ hT 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
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
rw : fst ≫ T.mor₁ = fst ≫ T.mor₁ + T.mor₂ ≫ inr - T.mor₂ ≫ inr
rw₁ rw₂ : fst ≫ T.mor₁ = fst ≫ T.mor₁
⊢ fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr

Tactic:
rw [← total, add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- 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
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
⊢ fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr

Tactic:
have eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr := by rw [← total, add_sub_cancel_right]
-- 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
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr
⊢ T.mor₁ ≫ fst = 𝟙 T.obj₁

Tactic:
simp only [← cancel_mono T.mor₁, assoc, id_comp, eq, comp_sub, comp_id,
            comp_distTriang_mor_zero₁₂_assoc _ hT, zero_comp, sub_zero]

Premises used: CategoryTheory.Category.assoc, sub_zero, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Limits.zero_comp, CategoryTheory.Pretriangulated.Triangle.mor₁, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CategoryTheory.Category.id_comp
-- 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
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr
⊢ inr ≫ fst = 0

Tactic:
simp only [← cancel_mono T.mor₁, assoc, eq, comp_sub, reassoc_of% inr_snd,
            comp_id, sub_self, zero_comp]

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Limits.zero_comp, CategoryTheory.Pretriangulated.Triangle.mor₁, CategoryTheory.Preadditive.comp_sub
-- 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
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr
⊢ BinaryBiproductData.{v, u} T.obj₁ T.obj₃

Tactic:
exact
    { bicone :=
      { pt := T.obj₂
        fst := fst
        snd := T.mor₂
        inl := T.mor₁
        inr := inr
        inl_fst := by
          simp only [← cancel_mono T.mor₁, assoc, id_comp, eq, comp_sub, comp_id,
            comp_distTriang_mor_zero₁₂_assoc _ hT, zero_comp, sub_zero]
        inl_snd := comp_distTriang_mor_zero₁₂ _ hT
        inr_fst := by
          simp only [← cancel_mono T.mor₁, assoc, eq, comp_sub, reassoc_of% inr_snd,
            comp_id, sub_self, zero_comp]
        inr_snd := inr_snd }
      isBilimit := isBinaryBilimitOfTotal _ total }
-- 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 :
  ∀ (X₂ : C) (inl : X₁ ⟶ X₂) (snd : X₂ ⟶ X₃)
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk inl snd 0)),
    HasBinaryBiproduct.{v, u} X₁ X₃
⊢ HasBinaryBiproduct.{v, u} X₁ X₃

Tactic:
obtain ⟨X₂, inl, snd, 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
⊢ Eq.{v + 1} (α := X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (Triangle.obj₁ (Triangle.mk inl snd 0)))
    (𝟙 X₃ ≫ Triangle.mor₃ (Triangle.mk inl snd 0)) 0

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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
obtain : ∀ (inr : X₃ ⟶ X₂) (inr_snd : 𝟙 X₃ = inr ≫ snd), HasBinaryBiproduct.{v, u} X₁ X₃
⊢ HasBinaryBiproduct.{v, u} X₁ X₃

Tactic:
obtain ⟨inr : X₃ ⟶ X₂, inr_snd : 𝟙 _ = inr ≫ snd⟩ :=
    Triangle.coyoneda_exact₃ _ mem (𝟙 X₃) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃
-- 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
dsimp : (𝟙 X₂ - snd ≫ inr) ≫ snd = 0
⊢ Eq (α := X₂ ⟶ Triangle.obj₃ (Triangle.mk inl snd 0)) ((𝟙 X₂ - snd ≫ inr) ≫ Triangle.mor₂ (Triangle.mk inl snd 0)) 0

Tactic:
dsimp
-- 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
⊢ (𝟙 X₂ - snd ≫ inr) ≫ snd = 0

Tactic:
simp only [sub_comp, assoc, id_comp, ← inr_snd, comp_id, sub_self]

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.Category.comp_id, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
obtain : ∀ (fst : X₂ ⟶ X₁) (hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl), HasBinaryBiproduct.{v, u} X₁ X₃
⊢ HasBinaryBiproduct.{v, u} X₁ X₃

Tactic:
obtain ⟨fst : X₂ ⟶ X₁, hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl⟩ :=
    Triangle.coyoneda_exact₂ _ mem (𝟙 X₂ - snd ≫ inr) (by
      dsimp
      simp only [sub_comp, assoc, id_comp, ← inr_snd, comp_id, sub_self])

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, HSub.hSub, CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp
-- 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
fst : X₂ ⟶ X₁
hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl
⊢ HasBinaryBiproduct.{v, u} X₁ X₃

Tactic:
⟨⟨binaryBiproductData _ mem rfl inr inr_snd.symm fst ?_⟩⟩

Premises used: CategoryTheory.Pretriangulated.binaryBiproductData, CategoryTheory.Limits.HasBinaryBiproduct.mk', Nonempty.intro, Eq.symm, 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
fst : X₂ ⟶ X₁
hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl
refine :
  HAdd.hAdd (α := Triangle.obj₂ (Triangle.mk inl snd 0) ⟶ Triangle.obj₂ (Triangle.mk inl snd 0)) (β :=
      Triangle.obj₂ (Triangle.mk inl snd 0) ⟶ Triangle.obj₂ (Triangle.mk inl snd 0))
      (fst ≫ Triangle.mor₁ (Triangle.mk inl snd 0)) (Triangle.mor₂ (Triangle.mk inl snd 0) ≫ inr) =
    𝟙 (Triangle.obj₂ (Triangle.mk inl snd 0))
⊢ HasBinaryBiproduct.{v, u} X₁ X₃

Tactic:
refine ⟨⟨binaryBiproductData _ mem rfl inr inr_snd.symm fst ?_⟩⟩
-- 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
fst : X₂ ⟶ X₁
hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl
dsimp : fst ≫ inl + snd ≫ inr = 𝟙 X₂
⊢ HAdd.hAdd (α := Triangle.obj₂ (Triangle.mk inl snd 0) ⟶ Triangle.obj₂ (Triangle.mk inl snd 0)) (β :=
      Triangle.obj₂ (Triangle.mk inl snd 0) ⟶ Triangle.obj₂ (Triangle.mk inl snd 0))
      (fst ≫ Triangle.mor₁ (Triangle.mk inl snd 0)) (Triangle.mor₂ (Triangle.mk inl snd 0) ≫ inr) =
    𝟙 (Triangle.obj₂ (Triangle.mk inl snd 0))

Tactic:
dsimp
-- 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₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk inl snd 0)
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
fst : X₂ ⟶ X₁
hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl
⊢ fst ≫ inl + snd ≫ inr = 𝟙 X₂

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
⊢ HasFiniteProducts.{v, u} C

Tactic:
hasFiniteProducts_of_has_binary_and_terminal

Premises used: CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal
-- 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
⊢ HasFiniteCoproducts.{v, u} C

Tactic:
hasFiniteCoproducts_of_has_binary_and_initial

Premises used: CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial
-- 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
⊢ HasFiniteBiproducts.{v, u} C

Tactic:
HasFiniteBiproducts.of_hasFiniteProducts

Premises used: CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
-- 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
⊢ Epi T.mor₂

Tactic:
have := T.epi₂ hT zero
-- 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 : Epi T.mor₂
⊢ IsSplitEpi T.mor₂

Tactic:
have := isSplitEpi_of_epi T.mor₂
-- 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₂
⊢ (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) ≫ T.mor₂ = 0

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
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₂
obtain :
  ∀ (fst : T.obj₂ ⟶ T.obj₁) (hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁),
    ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
⊢ ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
obtain ⟨fst, hfst⟩ := T.coyoneda_exact₂ hT (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) (by simp)

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, HSub.hSub, CategoryTheory.CategoryStruct.id, CategoryTheory.Pretriangulated.Triangle.mor₂, CategoryTheory.CategoryStruct.comp, CategoryTheory.section_, CategoryTheory.Pretriangulated.Triangle.obj₂
-- 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₁
⊢ section_ T.mor₂ ≫ T.mor₂ = 𝟙 T.obj₃

Tactic:
simp