awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
hf :
  Eq (α :=
    (shiftFunctor C (A := ℤ) 1 ⋙ F).obj (X.ω₁.obj (mk₁ f)) ⟶ (F ⋙ shiftFunctor D (A := ℤ) 1).obj (Y.ω₁.obj (mk₁ f)))
    ((shiftFunctor C (A := ℤ) 1 ⋙ F).map (α.hom.app (mk₁ f)) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      (F ⋙ shiftFunctor D (A := ℤ) 1).map (α.hom.app (mk₁ f)))
dsimp :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    ((F.map (X.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f))) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
⊢ Eq (α :=
    (Triangulated.SpectralObject.ω₁ (X.mapTriangulatedFunctor F)).obj (mk₁ g) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1)
        ((Triangulated.SpectralObject.ω₁ (Y.mapTriangulatedFunctor F)).obj (mk₁ f)))
    (Triangulated.SpectralObject.δ (X.mapTriangulatedFunctor F) f g ≫
      map (shiftFunctor D (A := ℤ) 1) ((whiskerRight α.hom F).app (mk₁ f)))
    ((whiskerRight α.hom F).app (mk₁ g) ≫ Triangulated.SpectralObject.δ (Y.mapTriangulatedFunctor F) f g)

Tactic:
dsimp at hf ⊢
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₁
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₂ : P T.obj₂
h₃ : P T.obj₃
⊢ P.isoClosure T.obj₁

Tactic:
IsTriangulatedClosed₁.ext₁' T hT h₂ h₃

Premises used: CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.ext₁'
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₂
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : P T.obj₁
h₃ : P T.obj₃
⊢ P.isoClosure T.obj₂

Tactic:
IsTriangulatedClosed₂.ext₂' T hT h₁ h₃

Premises used: CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.ext₂'
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₃
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : P T.obj₁
h₂ : P T.obj₂
⊢ P.isoClosure T.obj₃

Tactic:
IsTriangulatedClosed₃.ext₃' T hT h₁ h₂

Premises used: CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.ext₃'
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
obtain :
  ∀ (Z : C) (b : Y ⟶ Z) (c : 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 a b c)),
    ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : 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 a b c)
⊢ ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : 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 a b c)

Tactic:
obtain ⟨Z, b, c, h⟩ := distinguished_cocone_triangle a

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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
Z : C
b : Y ⟶ Z
c : 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 a b c)
obtain :
  ∀ (Z' : C) (hZ' : P Z') (e : (Triangle.mk a b c).obj₃ ≅ Z'),
    ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : 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 a b c)
⊢ ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : 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 a b c)

Tactic:
obtain ⟨Z', hZ', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₃' _ h hX hY

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃'
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
Z : C
b : Y ⟶ Z
c : 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 a b c)
Z' : C
hZ' : P Z'
e : (Triangle.mk a b c).obj₃ ≅ Z'
⊢ ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : 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 a b c)

Tactic:
⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm )⟩

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Pretriangulated.isomorphic_distinguished, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
Z : C
b : Y ⟶ Z
c : 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 a b c)
Z' : C
hZ' : P Z'
e : (Triangle.mk a b c).obj₃ ≅ Z'
⊢ ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : 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 a b c)

Tactic:
exact ⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
obtain :
  ∀ (X : C) (a : X ⟶ Y) (c : 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 a b c)),
    ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : 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 a b c)
⊢ ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : 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 a b c)

Tactic:
obtain ⟨X, a, c, h⟩ := distinguished_cocone_triangle₁ b

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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : 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 a b c)
obtain :
  ∀ (X' : C) (hX' : P X') (e : (Triangle.mk a b c).obj₁ ≅ X'),
    ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : 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 a b c)
⊢ ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : 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 a b c)

Tactic:
obtain ⟨X', hX', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₁' _ h hY hZ

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁'
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : 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 a b c)
X' : C
hX' : P X'
e : (Triangle.mk a b c).obj₁ ≅ X'
⊢ ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : 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 a b c)

Tactic:
⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Iso.refl, CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Pretriangulated.isomorphic_distinguished, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : 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 a b c)
X' : C
hX' : P X'
e : (Triangle.mk a b c).obj₁ ≅ X'
⊢ ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : 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 a b c)

Tactic:
exact ⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hX : P X
hZ : P Z
obtain :
  ∀ (Y : C) (a : X ⟶ Y) (b : Y ⟶ Z)
    (h :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk a b c)),
    ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk a b c)
⊢ ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)

Tactic:
obtain ⟨Y, a, b, h⟩ := distinguished_cocone_triangle₂ c

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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk a b c)
obtain :
  ∀ (Y' : C) (hY' : P Y') (e : (Triangle.mk a b c).obj₂ ≅ Y'),
    ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk a b c)
⊢ ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)

Tactic:
obtain ⟨Y', hY', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ h hX hZ

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂'
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk a b c)
Y' : C
hY' : P Y'
e : (Triangle.mk a b c).obj₂ ≅ Y'
⊢ ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)

Tactic:
⟨Y', hY', a ≫ e.hom, e.inv ≫ b, isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _))⟩

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Pretriangulated.isomorphic_distinguished, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk a b c)
Y' : C
hY' : P Y'
e : (Triangle.mk a b c).obj₂ ≅ Y'
⊢ ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)

Tactic:
exact ⟨Y', hY', a ≫ e.hom, e.inv ≫ b, isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _))⟩
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₁
inst_7 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₂ : P T.obj₂
h₃ : P T.obj₃
⊢ P T.obj₁

Tactic:
simpa only [isoClosure_eq_self] using P.ext_of_isTriangulatedClosed₁' T hT h₂ h₃

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁', CategoryTheory.ObjectProperty.isoClosure_eq_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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₂
inst_7 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : P T.obj₁
h₃ : P T.obj₃
⊢ P T.obj₂

Tactic:
simpa only [isoClosure_eq_self] using P.ext_of_isTriangulatedClosed₂' T hT h₁ h₃

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂', CategoryTheory.ObjectProperty.isoClosure_eq_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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulatedClosed₃
inst_7 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : P T.obj₁
h₂ : P T.obj₂
⊢ P T.obj₃

Tactic:
simpa only [isoClosure_eq_self] using P.ext_of_isTriangulatedClosed₃' T hT h₁ h₂

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃', CategoryTheory.ObjectProperty.isoClosure_eq_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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
hP :
  ∀ (T : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
      P T.obj₂ → P T.obj₃ → P T.obj₁
⊢ ∀ (T : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
      P T.obj₂ → P T.obj₃ → P.isoClosure T.obj₁

Tactic:
simpa only [isoClosure_eq_self] using hP

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
hP :
  ∀ (T : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
      P T.obj₁ → P T.obj₃ → P T.obj₂
⊢ ∀ (T : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
      P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂

Tactic:
simpa only [isoClosure_eq_self] using hP

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self