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 Y : C
φ : P.trW.RightFraction X Y
obtain :
  ∀ (Z : C) (f : X ⟶ Z) (g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW)))
    (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.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)

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

Premises used: CategoryTheory.MorphismProperty.RightFraction.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.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
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 :
  ∀ (Y' : C) (s' : Y ⟶ Y') (f' : Y' ⟶ Z)
    (mem' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))),
    ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)

Tactic:
obtain ⟨Y', s', f', mem'⟩ := distinguished_cocone_triangle₂ (g ≫ φ.f⟦1⟧')

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.MorphismProperty.RightFraction.f, CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, OfNat.ofNat
-- 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.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
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
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))
⊢ (Triangle.mk (φ.s (W := P.trW)) f g).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)) =
    𝟙 Z ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).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.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
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
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))
obtain :
  ∀
    (b :
      (Triangle.mk (φ.s (W := P.trW)) f g).obj₂ ⟶
        (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).obj₂)
    (hb₁ :
      (Triangle.mk (φ.s (W := P.trW)) f g).mor₁ ≫ b =
        φ.f (W := P.trW) ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₁),
    (Triangle.mk (φ.s (W := P.trW)) f g).mor₂ ≫ 𝟙 Z =
        b ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₂ →
      ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)

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

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.RightFraction.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.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
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
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))
b :
  (Triangle.mk (φ.s (W := P.trW)) f g).obj₂ ⟶
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).obj₂
hb₁ :
  (Triangle.mk (φ.s (W := P.trW)) f g).mor₁ ≫ b =
    φ.f (W := P.trW) ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₁
right :
  (Triangle.mk (φ.s (W := P.trW)) f g).mor₂ ≫ 𝟙 Z =
    b ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₂
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)

Tactic:
⟨MorphismProperty.LeftFraction.mk b s' ⟨_, _, _, mem', mem⟩, hb₁.symm⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction.mk, Exists.intro, Eq.symm
-- 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.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
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
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))
b :
  (Triangle.mk (φ.s (W := P.trW)) f g).obj₂ ⟶
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).obj₂
hb₁ :
  (Triangle.mk (φ.s (W := P.trW)) f g).mor₁ ≫ b =
    φ.f (W := P.trW) ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₁
right :
  (Triangle.mk (φ.s (W := P.trW)) f g).mor₂ ≫ 𝟙 Z =
    b ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₂
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)

Tactic:
exact ⟨MorphismProperty.LeftFraction.mk b s' ⟨_, _, _, mem', mem⟩, hb₁.symm⟩
-- 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₂
rw : s ≫ f₁ - s ≫ f₂ = 0
rw₁ : s ≫ f₂ - s ≫ f₂ = 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := X' ⟶ Y) 0 0
⊢ s ≫ (f₁ - f₂) = 0

Tactic:
rw [comp_sub, hf₁, sub_self]

Premises used: sub_self, CategoryTheory.Preadditive.comp_sub
-- 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₂
⊢ s ≫ (f₁ - f₂) = 0

Tactic:
have hf₂ : s ≫ (f₁ - f₂) = 0 := by rw [comp_sub, 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
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
obtain :
  ∀ (q : (Triangle.mk s g h).obj₃ ⟶ Y) (hq : f₁ - f₂ = (Triangle.mk s g h).mor₂ ≫ q),
    ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.trW t), f₁ ≫ t = f₂ ≫ t
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.trW t), f₁ ≫ t = f₂ ≫ t

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

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_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
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
obtain :
  ∀ (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)),
    ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.trW t), f₁ ≫ t = f₂ ≫ t
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.trW t), f₁ ≫ t = f₂ ≫ t

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

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- 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)
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.trW t), f₁ ≫ t = f₂ ≫ t

Tactic:
⟨Y', r, ?_, ?_⟩

Premises used: 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' 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)
refine_1 : P.trW r
refine_2 : f₁ ≫ r = f₂ ≫ r
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.trW t), f₁ ≫ t = f₂ ≫ t

Tactic:
refine ⟨Y', r, ?_, ?_⟩
-- 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)
⊢ P.trW r

Tactic:
⟨_, _, _, rot_of_distTriang _ mem', P.le_shift _ _ mem⟩

Premises used: CategoryTheory.ObjectProperty.trW, Exists.intro, CategoryTheory.Pretriangulated.rot_of_distTriang, CategoryTheory.ObjectProperty.le_shift
-- 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)
⊢ P.trW r

Tactic:
exact ⟨_, _, _, rot_of_distTriang _ mem', P.le_shift _ _ mem⟩