awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
⊢ f = 0
have hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
Tactic: have hg' : ∀ j, (g ≫ Pi.π _ j) ≫ (T j).mor₂ = 0 := fun j => by
      have : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π _ j = 0 := by
        rw [← reassoc_of% hg, reassoc_of% hf, zero_comp]
      rw [φ'.comm₂_assoc, h₂, id_comp] at this
      simpa using this
-- 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 φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
⊢ f = 0
have hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
Tactic: have hg'' := fun j => (T j).coyoneda_exact₂ (hT j) _ (hg' j)
-- 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 φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
⊢ f = 0
have hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
Tactic: have hα : ∀ j, _ = α j ≫ _ := fun j => (hg'' j).choose_spec
-- 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₁
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₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
⊢ g = Pi.lift α ≫ T'.mor₁
have dsimp : g =
  CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (b : J) ↦ (T b).obj₁) (Pi.lift α)
    (Limits.Pi.map fun (j : J) ↦ (T j).mor₁)
Tactic: dsimp [f₁, T']
-- 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₁
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₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
⊢ g =
    CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (b : J) ↦ (T b).obj₁) (Pi.lift α)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₁)
have h : ∀ (j : J),
  g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j =
    CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂)
      (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (b : J) ↦ (T b).obj₁) (Pi.lift α)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₁))
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j)
Tactic: ext j
-- 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₁
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₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
j : J
⊢ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j =
    CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂)
      (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (b : J) ↦ (T b).obj₁) (Pi.lift α)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₁))
      (Pi.π (fun (j : J) ↦ (T j).obj₂) j)
have h : α j ≫ (T j).mor₁ =
  CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂)
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (b : J) ↦ (T b).obj₁) (Pi.lift α)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₁))
    (Pi.π (fun (j : J) ↦ (T j).obj₂) j)
Tactic: rw [hα]
-- 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 φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
⊢ f = 0
have hg''' : g = Pi.lift α ≫ T'.mor₁
Tactic: have hg''' : g = Pi.lift α ≫ T'.mor₁ := by dsimp [f₁, T']; ext j; rw [hα]; 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
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₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
hg''' : g = Pi.lift α ≫ T'.mor₁
⊢ f = 0
have refine_1 : g ≫ T'.mor₂ = 0
Tactic: rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]
-- 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₁
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₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
hg''' : g = Pi.lift α ≫ T'.mor₁
refine_1 : g ≫ T'.mor₂ = 0
⊢ f = 0
have refine_1₁ : (Pi.lift α ≫ T'.mor₁) ≫ T'.mor₂ = 0
Tactic: rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]
-- 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₁
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₂
this_1 : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A_1 A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ (g_1 : A ⟶ (T j).obj₁), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ :=
  fun (j : J) ↦ ⋯.choose (p := fun (g_1 : A ⟶ (T j).obj₁) ↦ g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁)
hα : ∀ (j : J), g ≫ Pi.π (fun (j : J) ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
hg''' : g = Pi.lift α ≫ T'.mor₁
refine_1 : g ≫ T'.mor₂ = 0
refine_1₁ : (Pi.lift α ≫ T'.mor₁) ≫ T'.mor₂ = 0
⊢ f = 0
have refine_1₂ : Pi.lift α ≫ T'.mor₁ ≫ T'.mor₂ = 0
Tactic: rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]