awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s g h)
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
hf₂ : s ≫ (f₁ - f₂) = 0
q : (Triangle.mk s g h).obj₃ ⟶ Y
hq : f₁ - f₂ = (Triangle.mk s g h).mor₂ ≫ q
Y' : C
r : Y ⟶ Y'
t : Y' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Triangle.mk s g h).obj₃
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk q r t)
⊢ (Triangle.mk q r t).mor₁ ≫ (Triangle.mk q r t).mor₂ = 0

Tactic:
have eq := comp_distTriang_mor_zero₁₂ _ mem'
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s g h)
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
hf₂ : s ≫ (f₁ - f₂) = 0
q : (Triangle.mk s g h).obj₃ ⟶ Y
hq : f₁ - f₂ = (Triangle.mk s g h).mor₂ ≫ q
Y' : C
r : Y ⟶ Y'
t : Y' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Triangle.mk s g h).obj₃
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk q r t)
eq : q ≫ r = 0
refine_2 : f₁ ≫ r - f₂ ≫ r = 0
refine_2₁ : (f₁ - f₂) ≫ r = 0
refine_2₂ : ((Triangle.mk s g h).mor₂ ≫ q) ≫ r = 0
refine_2₃ : (Triangle.mk s g h).mor₂ ≫ q ≫ r = 0
refine_2₄ : Eq (α := X ⟶ Y') ((Triangle.mk s g h).mor₂ ≫ 0) 0
refine_2₅ refine_2₆ : Eq.{v_1 + 1} (α := X ⟶ Y') 0 0
⊢ f₁ ≫ r = f₂ ≫ r

Tactic:
rw [← sub_eq_zero, ← sub_comp, hq, assoc, eq, comp_zero]

Premises used: CategoryTheory.Category.assoc, sub_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
obtain :
  ∀ (Z : C) (f : φ.Y' (W := P.trW) ⟶ Z) (g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y)
    (H :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk (φ.s (W := P.trW)) f g))
    (mem : P Z),
    ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)
⊢ ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)

Tactic:
obtain ⟨Z, f, g, H, mem⟩ := φ.hs

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' (W := P.trW) ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
obtain :
  ∀ (X' : C) (f' : X' ⟶ X) (h' : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X')
    (mem' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h')),
    ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)
⊢ ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)

Tactic:
obtain ⟨X', f', h', mem'⟩ := distinguished_cocone_triangle₁ (φ.f ≫ f)

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' (W := P.trW) ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h')
⊢ (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₂ ≫ 𝟙 Z = φ.f (W := P.trW) ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' (W := P.trW) ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h')
obtain :
  ∀ (a : (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').obj₁ ⟶ (Triangle.mk (φ.s (W := P.trW)) f g).obj₁)
    (ha₁ :
      (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₁ ≫ φ.f (W := P.trW) =
        a ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₁),
    (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a =
        𝟙 Z ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₃ →
      ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)
⊢ ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)

Tactic:
obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ _
      mem' H φ.f (𝟙 Z) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' (W := P.trW) ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h')
a : (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').obj₁ ⟶ (Triangle.mk (φ.s (W := P.trW)) f g).obj₁
ha₁ : (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₁ ≫ φ.f (W := P.trW) = a ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₁
right :
  (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a =
    𝟙 Z ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₃
⊢ ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)

Tactic:
⟨MorphismProperty.RightFraction.mk f' ⟨_, _, _, mem', mem⟩ a, ha₁⟩

Premises used: CategoryTheory.MorphismProperty.RightFraction.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' (W := P.trW) ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h')
a : (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').obj₁ ⟶ (Triangle.mk (φ.s (W := P.trW)) f g).obj₁
ha₁ : (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₁ ≫ φ.f (W := P.trW) = a ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₁
right :
  (Triangle.mk f' (φ.f (W := P.trW) ≫ f) h').mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a =
    𝟙 Z ≫ (Triangle.mk (φ.s (W := P.trW)) f g).mor₃
⊢ ∃ (ψ : P.trW.RightFraction X Y), ψ.s (W := P.trW) ≫ φ.f (W := P.trW) = ψ.f (W := P.trW) ≫ φ.s (W := P.trW)

Tactic:
exact ⟨MorphismProperty.RightFraction.mk f' ⟨_, _, _, mem', mem⟩ a, ha₁⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z Z' : C
f₁ f₂ : Y ⟶ Z
s : Z ⟶ Z'
hs : P.trW s
hf₁ : f₁ ≫ s = f₂ ≫ s
⊢ ∃ (X : C) (f : X ⟶ Z) (h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f s h)),
    P X

Tactic:
rw [P.trW_iff'] at hs

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z Z' : C
f₁ f₂ : Y ⟶ Z
s : Z ⟶ Z'
hs : P.trW s
hf₁ : f₁ ≫ s = f₂ ≫ s
hs₁ :
  ∃ (X : C) (f : X ⟶ Z) (h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f s h)),
    P X
⊢ f₁ ≫ s = f₂ ≫ s

Tactic:
rw [P.trW_iff'] at hs

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z Z' : C
f₁ f₂ : Y ⟶ Z
s : Z ⟶ Z'
hs :
  ∃ (X : C) (f : X ⟶ Z) (h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f s h)),
    P X
hf₁ : f₁ ≫ s = f₂ ≫ s
obtain :
  ∀ (Z_1 : C) (g : Z_1 ⟶ Z) (h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z_1)
    (H :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g s h))
    (mem : P Z_1), ∃ (X' : C) (t : X' ⟶ Y) (_ : P.trW t), t ≫ f₁ = t ≫ f₂
⊢ ∃ (X' : C) (t : X' ⟶ Y) (_ : P.trW t), t ≫ f₁ = t ≫ f₂

Tactic:
obtain ⟨Z, g, h, H, mem⟩ := hs
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z_1 Z' : C
f₁ f₂ : Y ⟶ Z_1
s : Z_1 ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z_1
h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g s h)
mem : P Z
rw : f₁ ≫ s - f₂ ≫ s = 0
rw₁ : f₂ ≫ s - f₂ ≫ s = 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := Y ⟶ Z') 0 0
⊢ (f₁ - f₂) ≫ s = 0

Tactic:
rw [sub_comp, hf₁, sub_self]

Premises used: sub_self, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z_1 Z' : C
f₁ f₂ : Y ⟶ Z_1
s : Z_1 ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z_1
h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g s h)
mem : P Z
⊢ (f₁ - f₂) ≫ s = 0

Tactic:
have hf₂ : (f₁ - f₂) ≫ s = 0 := by rw [sub_comp, hf₁, sub_self]
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z_1 Z' : C
f₁ f₂ : Y ⟶ Z_1
s : Z_1 ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z_1
h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g s h)
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
obtain :
  ∀ (q : Y ⟶ (Triangle.mk g s h).obj₁) (hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁),
    ∃ (X' : C) (t : X' ⟶ Y) (_ : P.trW t), t ≫ f₁ = t ≫ f₂
⊢ ∃ (X' : C) (t : X' ⟶ Y) (_ : P.trW t), t ≫ f₁ = t ≫ f₂

Tactic:
obtain ⟨q, hq⟩ := Triangle.coyoneda_exact₂ _ H _ hf₂

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
Y Z_1 Z' : C
f₁ f₂ : Y ⟶ Z_1
s : Z_1 ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z_1
h : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g s h)
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
q : Y ⟶ (Triangle.mk g s h).obj₁
hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁
obtain :
  ∀ (Y' : C) (r : Y' ⟶ Y)
    (t : (Triangle.mk g s h).obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y')
    (mem' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk r q t)),
    ∃ (X' : C) (t : X' ⟶ Y) (_ : P.trW t), t ≫ f₁ = t ≫ f₂
⊢ ∃ (X' : C) (t : X' ⟶ Y) (_ : P.trW t), t ≫ f₁ = t ≫ f₂

Tactic:
obtain ⟨Y', r, t, mem'⟩ := distinguished_cocone_triangle₁ q

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁