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 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)
⊢ Triangle.mor₁
        (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))))) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂.{v_1, u_1}
            (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))))))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₁.{v_1, u_1}
            (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).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
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)
⊢ Triangle.mor₂
        (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))))) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₃.{v_1, u_1}
            (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))))))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₂.{v_1, u_1}
            (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).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
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)
⊢ (Triangle.mor₃
          (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))))) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1)
          (Iso.hom
            (Iso.refl
              (Triangle.obj₁.{v_1, u_1}
                (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))))))))).op =
    (Iso.hom
          (Iso.refl
            (Triangle.obj₃.{v_1, u_1}
              (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).mor₃).op

Tactic:
simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]

Premises used: CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app
-- 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)
⊢ 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

Tactic:
exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
    (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))

Premises used: Quiver.Hom.op_inj, CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- 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₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
rw :
  ∀
    (hT₁ :
      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₁)))
    (hT₂ :
      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₂)))
    (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
rw [mem_distinguishedTriangles_iff] at hT₁ hT₂

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
T₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
hT₁ :
  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₁))
hT₂ :
  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₂))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
obtain :
  ∀
    (c :
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₂)).obj₁ ⟶
        (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₁)).obj₁)
    (hc₁ :
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₂)).mor₁ ≫ b.unop =
        c ≫ (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₁)).mor₁)
    (hc₂ :
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₂)).mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) c =
        a.unop ≫ (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₁)).mor₃),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
obtain ⟨c, hc₁, hc₂⟩ :=
    Pretriangulated.complete_distinguished_triangle_morphism₁ _ _ hT₂ hT₁
      b.unop a.unop (Quiver.Hom.op_inj comm.symm)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁, Eq.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₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
hT₁ :
  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₁))
hT₂ :
  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₂))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₃.unop ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₂.obj₁) ≫
      a.unop ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₁.obj₁) :
            Opposite.unop T₁.obj₁ ⟶
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))))
          (Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₃.unop :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃)))
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
⟨c.op, Quiver.Hom.unop_inj hc₁.symm, Quiver.Hom.unop_inj ?_⟩

Premises used: Quiver.Hom.op, Quiver.Hom.unop_inj, And.intro, Exists.intro, Eq.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₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
hT₁ :
  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₁))
hT₂ :
  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₂))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₃.unop ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₂.obj₁) ≫
      a.unop ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₁.obj₁) :
            Opposite.unop T₁.obj₁ ⟶
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))))
          (Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₃.unop :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃)))
refine : Quiver.Hom.unop (T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a) = Quiver.Hom.unop (c.op ≫ T₂.mor₃)
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
refine ⟨c.op, Quiver.Hom.unop_inj hc₁.symm, Quiver.Hom.unop_inj ?_⟩
-- 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₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
hT₁ :
  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₁))
hT₂ :
  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₂))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₃.unop ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₂.obj₁) ≫
      a.unop ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₁.obj₁) :
            Opposite.unop T₁.obj₁ ⟶
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))))
          (Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₃.unop :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃)))
a₁ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Quiver.Hom.unop (T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a)))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Quiver.Hom.unop (c.op ≫ T₂.mor₃)))
⊢ Quiver.Hom.unop (T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a) = Quiver.Hom.unop (c.op ≫ T₂.mor₃)

Tactic:
apply (shiftFunctor C (1 : ℤ)).map_injective

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_injective, OfNat.ofNat
-- 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ᵒᵖ)) (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
      T ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
      (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T))

Tactic:
rfl
-- 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ᵒᵖ)) (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
      T ↔
    ∃ (T' : Triangle.{v_1, u_1} C) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) T'),
      Nonempty.{v_1 + 1} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
Opposite.mem_distinguishedTriangles_iff' T

Premises used: CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff', Set.Mem