awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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₂
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
have refine_2₅ : y₂ = y₂
Tactic: rw [add_comp, assoc, φ.comm₁, reassoc_of% hx₁, ← hy₁, add_sub_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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 (rotate C) T).obj₃) (TriangleMorphism.hom₃ (Functor.map (rotate C) φ))
have dsimp : IsIso (X := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁)
  (Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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 (invRotate C) T).obj₁) (TriangleMorphism.hom₁ (Functor.map (invRotate C) φ))
have dsimp : IsIso (X := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃)
  (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
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₂
⊢ BinaryBiproductData.{v, u} T.obj₁ T.obj₃
have this : Mono T.mor₁
Tactic: have : Mono T.mor₁ := T.mono₁ hT hT₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
have rw : fst ≫ T.mor₁ = fst ≫ T.mor₁ + T.mor₂ ≫ inr - T.mor₂ ≫ inr
Tactic: rw [← total, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
⊢ fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr
have rw₁ : fst ≫ T.mor₁ = fst ≫ T.mor₁
Tactic: rw [← total, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
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₁
⊢ BinaryBiproductData.{v, u} T.obj₁ T.obj₃
have eq : 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
⊢ HasBinaryBiproduct.{v, u} X₁ X₃
have 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₃
Tactic: obtain ⟨X₂, inl, snd, mem⟩ := distinguished_cocone_triangle₂ (0 : X₃ ⟶ X₁⟦(1 : ℤ)⟧)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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)
⊢ HasBinaryBiproduct.{v, u} X₁ X₃
have obtain : ∀ (inr : X₃ ⟶ X₂) (inr_snd : 𝟙 X₃ = inr ≫ snd), HasBinaryBiproduct.{v, u} X₁ X₃
Tactic: obtain ⟨inr : X₃ ⟶ X₂, inr_snd : 𝟙 _ = inr ≫ snd⟩ :=
    Triangle.coyoneda_exact₃ _ mem (𝟙 X₃) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
⊢ Eq (α := X₂ ⟶ Triangle.obj₃ (Triangle.mk inl snd 0)) ((𝟙 X₂ - snd ≫ inr) ≫ Triangle.mor₂ (Triangle.mk inl snd 0)) 0
have dsimp : (𝟙 X₂ - snd ≫ inr) ≫ snd = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
⊢ HasBinaryBiproduct.{v, u} X₁ X₃
have obtain : ∀ (fst : X₂ ⟶ X₁) (hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl), 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])
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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₃
have 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))
Tactic: refine ⟨⟨binaryBiproductData _ mem rfl inr inr_snd.symm fst ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
⊢ 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))
have dsimp : fst ≫ inl + snd ≫ inr = 𝟙 X₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
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
⊢ ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
have this : Epi T.mor₂
Tactic: have := T.epi₂ hT zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
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₂
⊢ ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
have this₁ : IsSplitEpi T.mor₂
Tactic: have := isSplitEpi_of_epi T.mor₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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₂
⊢ ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
have 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
Tactic: obtain ⟨fst, hfst⟩ := T.coyoneda_exact₂ hT (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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 ⋯
⊢ ∃ (e : T.obj₂ ≅ biprod.{v, u} T.obj₁ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd
have 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
Tactic: refine ⟨biprod.uniqueUpToIso _ _ d.isBilimit, ⟨?_, by simp [d]⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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 ⋯
⊢ Eq (α := T.obj₁ ⟶ biprod.{v, u} T.obj₁ T.obj₃) (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit))
    biprod.inl
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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
⊢ Eq (α := T.obj₁ ⟶ biprod.{v, u} T.obj₁ T.obj₃) (T.mor₁ ≫ Iso.hom (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit))
    biprod.inl
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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 _)
    (binaryBiproductTriangle X₁ X₂)
have 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₂)
Tactic: obtain ⟨Y, g, h, mem⟩ := distinguished_cocone_triangle₂ (0 : X₂ ⟶ X₁⟦(1 : ℤ)⟧)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (binaryBiproductTriangle X₁ X₂)
have 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₂)
Tactic: obtain ⟨e, ⟨he₁, he₂⟩⟩ := exists_iso_binaryBiproduct_of_distTriang _ mem rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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₂)
have refine : Iso (C := Triangle.{v, u} C) (Triangle.mk g h 0) (binaryBiproductTriangle X₁ X₂)
Tactic: refine isomorphic_distinguished _ mem _ (Iso.symm ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
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₁
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (productTriangle T)
have 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)
Tactic: obtain ⟨Z, f₂, f₃, hT'⟩ := distinguished_cocone_triangle f₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
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 φ
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (productTriangle T)
have h₁ : φ'.hom₁ = 𝟙 T'.obj₁
Tactic: have h₁ : φ'.hom₁ = 𝟙 _ := by cat_disch