ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : T.mor₃ = 0<GOAL>CategoryTheory.Epi T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : T.mor₂ = 0<GOAL>CategoryTheory.Epi T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : T.mor₁ = 0<GOAL>CategoryTheory.Epi T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₁ = 0 ↔ CategoryTheory.Mono T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₂ = 0 ↔ CategoryTheory.Mono T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>T.mor₃ = 0 ↔ CategoryTheory.Mono T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Mono T.mor₂<GOAL>T.mor₁ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Mono T.mor₃<GOAL>T.mor₂ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.Mono T.mor₁<GOAL>T.mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : T.mor₁ = 0<GOAL>CategoryTheory.Mono T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : T.mor₂ = 0<GOAL>CategoryTheory.Mono T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : T.mor₃ = 0<GOAL>CategoryTheory.Mono T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>CategoryTheory.Limits.IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>CategoryTheory.Limits.IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>CategoryTheory.Limits.IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₂ : CategoryTheory.Limits.IsZero T.obj₂<VAR>h₃ : CategoryTheory.Limits.IsZero T.obj₃<GOAL>CategoryTheory.Limits.IsZero T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₁ : CategoryTheory.Limits.IsZero T.obj₁<VAR>h₃ : CategoryTheory.Limits.IsZero T.obj₃<GOAL>CategoryTheory.Limits.IsZero T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₁ : CategoryTheory.Limits.IsZero T.obj₁<VAR>h₂ : CategoryTheory.Limits.IsZero T.obj₂<GOAL>CategoryTheory.Limits.IsZero T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>CategoryTheory.Limits.IsZero T.obj₁ ↔ CategoryTheory.IsIso T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>CategoryTheory.Limits.IsZero T.obj₂ ↔ CategoryTheory.IsIso T.mor₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>CategoryTheory.Limits.IsZero T.obj₃ ↔ CategoryTheory.IsIso T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.IsIso T.mor₂<GOAL>CategoryTheory.Limits.IsZero T.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.IsIso T.mor₃<GOAL>CategoryTheory.Limits.IsZero T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : CategoryTheory.IsIso T.mor₁<GOAL>CategoryTheory.Limits.IsZero T.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n : ℤ<GOAL>(CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n).obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : T ⟶ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₁ : CategoryTheory.IsIso φ.hom₁<VAR>h₃ : CategoryTheory.IsIso φ.hom₃<GOAL>CategoryTheory.IsIso φ.hom₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : T ⟶ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₁ : CategoryTheory.IsIso φ.hom₁<VAR>h₂ : CategoryTheory.IsIso φ.hom₂<GOAL>CategoryTheory.IsIso φ.hom₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T T' : CategoryTheory.Pretriangulated.Triangle C<VAR>φ : T ⟶ T'<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₂ : CategoryTheory.IsIso φ.hom₂<VAR>h₃ : CategoryTheory.IsIso φ.hom₃<GOAL>CategoryTheory.IsIso φ.hom₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inr = inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.inl = T.mor₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).isBilimit = CategoryTheory.Limits.isBinaryBilimitOfTotal { pt := T.obj₂, fst := fst, snd := T.mor₂, inl := T.mor₁, inr := inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := inr_snd } total
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.fst = fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.snd = T.mor₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₀ : T.mor₃ = 0<VAR>inr : T.obj₃ ⟶ T.obj₂<VAR>inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃<VAR>fst : T.obj₂ ⟶ T.obj₁<VAR>total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂<GOAL>(CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.pt = T.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>zero : T.mor₃ = 0<GOAL>∃ e, T.mor₁ ≫ e.hom = CategoryTheory.Limits.biprod.inl ∧ T.mor₂ = e.hom ≫ CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>X₁ X₂ : C<GOAL>CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>X₁ X₂ : C<GOAL>CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>(CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₁ = a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>(CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₂ = b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>J : Type u_1<VAR>T : J → CategoryTheory.Pretriangulated.Triangle C<VAR>hT : ∀ (j : J), T j ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₁<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₂<VAR>CategoryTheory.Limits.HasProduct fun j => (T j).obj₃<VAR>CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁<GOAL>CategoryTheory.Pretriangulated.productTriangle T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>e : CategoryTheory.Arrow.mk T₁.mor₁ ≅ CategoryTheory.Arrow.mk T₂.mor₁<GOAL>∃ e', e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>e₁ : T₁.obj₁ ≅ T₂.obj₁<VAR>e₂ : T₁.obj₂ ≅ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁<GOAL>(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₂ = e₂.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>e₁ : T₁.obj₁ ≅ T₂.obj₁<VAR>e₂ : T₁.obj₂ ≅ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁<GOAL>(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₁ = e₁.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>e₁ : T₁.obj₁ ≅ T₂.obj₁<VAR>e₂ : T₁.obj₂ ≅ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁<GOAL>(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₂ = e₂.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : CategoryTheory.Pretriangulated C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C<VAR>hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>e₁ : T₁.obj₁ ≅ T₂.obj₁<VAR>e₂ : T₁.obj₂ ≅ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁<GOAL>(CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₁ = e₁.inv
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>self : CategoryTheory.EnrichedCategory V C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.EnrichedCategory.Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.id Y)) (CategoryTheory.EnrichedCategory.comp X Y Y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)