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
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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
⊢ a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
      a' ≫
        φ'.hom₃ ≫
          (productTriangle T).mor₃ ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    0
have rw : a ≫ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
    a' ≫
      T'.mor₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
  0
Tactic: rw [← φ'.comm₃_assoc]
-- 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
⊢ a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
      a' ≫
        T'.mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    0
have rw : a ≫ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
    a ≫
      (productTriangle T).mor₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
  0
Tactic: rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp]
-- 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
rw :
  a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
      a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    0
⊢ a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
      a' ≫
        T'.mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    0
have rw₁ : a ≫ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
  a ≫
    (productTriangle T).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j))
Tactic: rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp]
-- 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
rw :
  a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
      a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    0
rw₁ :
  a ≫
      (productTriangle T).mor₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    a ≫
      (productTriangle T).mor₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j))
⊢ a ≫
        (productTriangle T).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) -
      a' ≫
        T'.mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) φ'.hom₁ ≫
            Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
    0
have rw₂ : a ≫ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j)) =
  a ≫
    (productTriangle T).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 T'.obj₁) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) (TriangleMorphism.hom₁ (productTriangle.π T j))
Tactic: rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp]
-- 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
⊢ ∃ (a_1 : A ⟶ T'.obj₃), (fun (x : A ⟶ T'.obj₃) ↦ x ≫ φ'.hom₃) a_1 = a
have ha'' : ∀ (j : J), ∃ (g : A ⟶ (T j).obj₂), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂
Tactic: have ha'' := fun (j : J) => (T j).coyoneda_exact₃ (hT j) ((a - a' ≫ φ'.hom₃) ≫ Pi.π _ j) (by
      simp only [sub_comp, assoc]
      erw [← (productTriangle.π T j).comm₃]
      rw [← φ'.comm₃_assoc]
      rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp])
-- 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ (g : A ⟶ (T j).obj₂), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ :=
  fun (j : J) ↦
    ⋯.choose (p := fun (g : A ⟶ (T j).obj₂) ↦ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂)
⊢ ∃ (a_1 : A ⟶ T'.obj₃), (fun (x : A ⟶ T'.obj₃) ↦ x ≫ φ'.hom₃) a_1 = a
have hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
Tactic: have hb : ∀ j, _ = b j ≫ _ := fun j => (ha'' 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ (g : A ⟶ (T j).obj₂), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ :=
  fun (j : J) ↦
    ⋯.choose (p := fun (g : A ⟶ (T j).obj₂) ↦ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂)
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
j : J
⊢ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j =
    (Pi.lift b ≫ (productTriangle T).mor₂) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j
have rw : b j ≫ (T j).mor₂ = (Pi.lift b ≫ (productTriangle T).mor₂) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j
Tactic: rw [hb]
-- 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ (g : A ⟶ (T j).obj₂), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ :=
  fun (j : J) ↦
    ⋯.choose (p := fun (g : A ⟶ (T j).obj₂) ↦ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂)
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
⊢ ∃ (a_1 : A ⟶ T'.obj₃), (fun (x : A ⟶ T'.obj₃) ↦ x ≫ φ'.hom₃) a_1 = a
have hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂
Tactic: have hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂ :=
      Limits.Pi.hom_ext _ _ (fun j => by rw [hb]; 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 : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ (g : A ⟶ (T j).obj₂), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ :=
  fun (j : J) ↦
    ⋯.choose (p := fun (g : A ⟶ (T j).obj₂) ↦ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = g ≫ (T j).mor₂)
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun (j : J) ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂
⊢ (a' + Pi.lift b ≫ T'.mor₂) ≫ φ'.hom₃ = a
have rw : a' ≫ φ'.hom₃ + (Pi.lift b ≫ T'.mor₂) ≫ φ'.hom₃ = a
Tactic: rw [add_comp, assoc, φ'.comm₂, h₂, id_comp, ← hb', add_sub_cancel]