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₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
⊢ x₃ ≫ T.mor₃ = 0
have rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
⊢ x₃ ≫ T.mor₃ = 0
have rw₂ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₂ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0
⊢ x₃ ≫ T.mor₃ = 0
have rw₃ : x₃ ≫ φ.hom₃ ≫ T'.mor₃ = 0
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₂ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0
rw₃ : x₃ ≫ φ.hom₃ ≫ T'.mor₃ = 0
⊢ x₃ ≫ T.mor₃ = 0
have rw₄ : y₂ ≫ T'.mor₂ ≫ T'.mor₃ = 0
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₂ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0
rw₃ : x₃ ≫ φ.hom₃ ≫ T'.mor₃ = 0
rw₄ : y₂ ≫ T'.mor₂ ≫ T'.mor₃ = 0
⊢ x₃ ≫ T.mor₃ = 0
have rw₅ : Eq (α := A ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T'.obj₁) (y₂ ≫ 0) 0
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₂ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0
rw₃ : x₃ ≫ φ.hom₃ ≫ T'.mor₃ = 0
rw₄ : y₂ ≫ T'.mor₂ ≫ T'.mor₃ = 0
rw₅ : Eq (α := A ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T'.obj₁) (y₂ ≫ 0) 0
⊢ x₃ ≫ T.mor₃ = 0
have rw₆ : Eq.{v + 1} (α := A ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T'.obj₁) 0 0
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
have refine_2 : ∀ (x₂ : A ⟶ T.obj₂) (hx₂ : x₃ = x₂ ≫ T.mor₂), ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
Tactic: obtain ⟨x₂, hx₂⟩ := Triangle.coyoneda_exact₃ _ hT x₃
      (by rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        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
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₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
have rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
Tactic: rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₂
rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
have rw₁ : y₂ ≫ T'.mor₂ - x₂ ≫ φ.hom₂ ≫ T'.mor₂ = 0
Tactic: rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₂
rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
rw₁ : y₂ ≫ T'.mor₂ - x₂ ≫ φ.hom₂ ≫ T'.mor₂ = 0
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
have rw₂ : y₂ ≫ T'.mor₂ - x₂ ≫ T.mor₂ ≫ φ.hom₃ = 0
Tactic: rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₂
rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
rw₁ : y₂ ≫ T'.mor₂ - x₂ ≫ φ.hom₂ ≫ T'.mor₂ = 0
rw₂ : y₂ ≫ T'.mor₂ - x₂ ≫ T.mor₂ ≫ φ.hom₃ = 0
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
have rw₃ : y₂ ≫ T'.mor₂ - x₃ ≫ φ.hom₃ = 0
Tactic: rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₂
rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
rw₁ : y₂ ≫ T'.mor₂ - x₂ ≫ φ.hom₂ ≫ T'.mor₂ = 0
rw₂ : y₂ ≫ T'.mor₂ - x₂ ≫ T.mor₂ ≫ φ.hom₃ = 0
rw₃ : y₂ ≫ T'.mor₂ - x₃ ≫ φ.hom₃ = 0
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
have rw₄ : y₂ ≫ T'.mor₂ - y₂ ≫ T'.mor₂ = 0
Tactic: rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₂
rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
rw₁ : y₂ ≫ T'.mor₂ - x₂ ≫ φ.hom₂ ≫ T'.mor₂ = 0
rw₂ : y₂ ≫ T'.mor₂ - x₂ ≫ T.mor₂ ≫ φ.hom₃ = 0
rw₃ : y₂ ≫ T'.mor₂ - x₃ ≫ φ.hom₃ = 0
rw₄ : y₂ ≫ T'.mor₂ - y₂ ≫ T'.mor₂ = 0
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
have rw₅ : Eq.{v + 1} (α := A ⟶ T'.obj₃) 0 0
Tactic: rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
have refine_2 : ∀ (y₁ : A ⟶ T'.obj₁) (hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁),
  ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
Tactic: obtain ⟨y₁, hy₁⟩ := Triangle.coyoneda_exact₂ _ hT' (y₂ - x₂ ≫ φ.hom₂)
      (by rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, 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
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₁
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
have refine_2 : ∀ (x₁ : A ⟶ T.obj₁) (hx₁ : x₁ ≫ φ.hom₁ = y₁), ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
Tactic: obtain ⟨x₁, hx₁⟩ : ∃ (x₁ : A ⟶ T.obj₁), x₁ ≫ φ.hom₁ = y₁ := ⟨y₁ ≫ inv φ.hom₁, 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 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₁
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
have refine_2 : (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) (x₂ + x₁ ≫ T.mor₁) = y₂
Tactic: refine ⟨x₂ + x₁ ≫ 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 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₁
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
have refine_2 : x₂ ≫ φ.hom₂ + (x₁ ≫ T.mor₁) ≫ φ.hom₂ = 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₃
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₂
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
have refine_2₁ : x₂ ≫ φ.hom₂ + x₁ ≫ T.mor₁ ≫ φ.hom₂ = 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₃
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₂
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
have refine_2₂ : x₂ ≫ φ.hom₂ + x₁ ≫ φ.hom₁ ≫ T'.mor₁ = 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₃
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₂
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
have refine_2₃ : x₂ ≫ φ.hom₂ + y₁ ≫ T'.mor₁ = 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₃
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₂
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
have refine_2₄ : x₂ ≫ φ.hom₂ + (y₂ - x₂ ≫ φ.hom₂) = y₂
Tactic: rw [add_comp, assoc, φ.comm₁, reassoc_of% hx₁, ← hy₁, add_sub_cancel]