awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
rw :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0) ⟶
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) (-1)) (𝟙 0))) 0
rw₁ :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0) ⟶
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) (-1)) 0)) 0
rw₂ :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0) ⟶
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))
    (Quiver.Hom.op 0) 0
rw₃ rw₄ :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0) ⟶
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))
    0 0
⊢ Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0) ⟶
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))
    (Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))) 0

Tactic:
rw [← Functor.map_id, id_zero, Functor.map_zero, op_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.id_zero, CategoryTheory.Functor.map_id, CategoryTheory.Limits.op_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
⊢ Triangle.mor₁ (contractibleTriangle X) ≫ Iso.hom (Iso.refl (Triangle.obj₂.{v_1, u_1} (contractibleTriangle X))) =
    Iso.hom (Iso.refl (Triangle.obj₁.{v_1, u_1} (contractibleTriangle X))) ≫
      Triangle.mor₁
        (Functor.obj (Equivalence.functor (triangleOpEquivalence C))
          (Opposite.op (Triangle.invRotate (contractibleTriangle (Opposite.unop X)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
⊢ Triangle.mor₂ (contractibleTriangle X) ≫ Iso.hom (IsZero.iso ⋯ ⋯) =
    Iso.hom (Iso.refl (Triangle.obj₂.{v_1, u_1} (contractibleTriangle X))) ≫
      Triangle.mor₂
        (Functor.obj (Equivalence.functor (triangleOpEquivalence C))
          (Opposite.op (Triangle.invRotate (contractibleTriangle (Opposite.unop X)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
⊢ Triangle.mor₃ (contractibleTriangle X) ≫
      Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
        (Iso.hom (Iso.refl (Triangle.obj₁.{v_1, u_1} (contractibleTriangle X)))) =
    Iso.hom (IsZero.iso ⋯ ⋯) ≫
      Triangle.mor₃
        (Functor.obj (Equivalence.functor (triangleOpEquivalence C))
          (Opposite.op (Triangle.invRotate (contractibleTriangle (Opposite.unop X)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
rw :
  ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) T'),
    Nonempty.{v_1 + 1}
      (contractibleTriangle X ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) (contractibleTriangle X)

Tactic:
rw [mem_distinguishedTriangles_iff']

Premises used: CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
⊢ ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) T'),
    Nonempty.{v_1 + 1}
      (contractibleTriangle X ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop),
    ⟨contractibleTriangleIso X⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso, Exists.intro, CategoryTheory.Pretriangulated.contractible_distinguished, Opposite.unop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X : Cᵒᵖ
⊢ ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) T'),
    Nonempty.{v_1 + 1}
      (contractibleTriangle X ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
exact ⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop),
    ⟨contractibleTriangleIso X⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.mor₁ ≫
      Iso.hom
        (Iso.refl (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.obj₂) =
    Iso.hom
        (Iso.refl (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.obj₁) ≫
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ Quiver.Hom.op
      ((Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.mor₂ ≫
        Iso.hom (-Iso.unop (Iso.app (Equivalence.unitIso (opShiftFunctorEquivalence C 1)) T.obj₁))) =
    (Iso.hom
          (Iso.refl
            (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.obj₂) ≫
        (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).mor₂).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom
          (Iso.refl
            (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate.obj₁)) =
    Iso.hom (-Iso.unop (Iso.app (Equivalence.unitIso (opShiftFunctorEquivalence C 1)) T.obj₁)) ≫
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).mor₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
T : Triangle.{v_1, u_1} Cᵒᵖ
simp :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)) ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) T ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) T.rotate

Tactic:
simp only [mem_distinguishedTriangles_iff, Pretriangulated.rotate_distinguished_triangle
    ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop]

Premises used: CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff, CategoryTheory.Pretriangulated.Triangle.rotate, CategoryTheory.Pretriangulated.triangleOpEquivalence, Opposite.unop, CategoryTheory.Functor.obj, CategoryTheory.Pretriangulated.rotate_distinguished_triangle, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)) ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate

Tactic:
distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm

Premises used: CategoryTheory.Pretriangulated.Opposite.rotateTriangleOpEquivalenceInverseObjRotateUnopIso, CategoryTheory.Pretriangulated.distinguished_iff_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)) ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T.rotate)).rotate

Tactic:
exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm

Premises used: CategoryTheory.Pretriangulated.Opposite.rotateTriangleOpEquivalenceInverseObjRotateUnopIso, CategoryTheory.Pretriangulated.distinguished_iff_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X Y : Cᵒᵖ
f : X ⟶ Y
obtain :
  ∀ (Z : C) (g : Z ⟶ Opposite.unop Y)
    (h : Opposite.unop X ⟶ 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))
        (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk g f.unop h)),
    ∃ (Z : Cᵒᵖ) (g : Y ⟶ 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 C) (Triangle.mk f g h)
⊢ ∃ (Z : Cᵒᵖ) (g : Y ⟶ 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 C) (Triangle.mk f g h)

Tactic:
obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle₁ f.unop

Premises used: Quiver.Hom.unop, CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ 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))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk g f.unop h)
⊢ ∃ (Z : Cᵒᵖ) (g : Y ⟶ 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 C) (Triangle.mk f g h)

Tactic:
⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
    (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, ?_⟩

Premises used: Opposite, Quiver.Hom.op, CategoryTheory.shiftFunctor, CategoryTheory.Functor.map, Opposite.op, Exists.intro, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Iso.inv, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ 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))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk g f.unop h)
refine :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C)
    (Triangle.mk f g.op
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙ Equivalence.functor (opShiftFunctorEquivalence C 1))
          (Opposite.op Z))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (Opposite.op Z))
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) h.op)))
⊢ ∃ (Z : Cᵒᵖ) (g : Y ⟶ 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 C) (Triangle.mk f g h)

Tactic:
refine ⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
    (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ 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))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk g f.unop h)
simp :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
    (Opposite.unop
      (Functor.obj (Equivalence.inverse (triangleOpEquivalence C))
        (Triangle.mk f g.op
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C 1))
              (Opposite.op Z))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (Opposite.op Z))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) h.op)))))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C)
    (Triangle.mk f g.op
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙ Equivalence.functor (opShiftFunctorEquivalence C 1))
          (Opposite.op Z))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (Opposite.op Z))
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) h.op)))

Tactic:
simp only [mem_distinguishedTriangles_iff]

Premises used: CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ 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))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk g f.unop h)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
    (Opposite.unop
      (Functor.obj (Equivalence.inverse (triangleOpEquivalence C))
        (Triangle.mk f g.op
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C 1))
              (Opposite.op Z))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (Opposite.op Z))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) h.op)))))

Tactic:
Pretriangulated.isomorphic_distinguished _ H _ ?_

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} 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
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ 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))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk g f.unop h)
refine :
  Opposite.unop
      (Functor.obj (Equivalence.inverse (triangleOpEquivalence C))
        (Triangle.mk f g.op
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C 1))
              (Opposite.op Z))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (Opposite.op Z))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) h.op)))) ≅
    Triangle.mk g f.unop h
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
    (Opposite.unop
      (Functor.obj (Equivalence.inverse (triangleOpEquivalence C))
        (Triangle.mk f g.op
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C 1))
              (Opposite.op Z))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (Opposite.op Z))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) h.op)))))

Tactic:
refine Pretriangulated.isomorphic_distinguished _ H _ ?_

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished