awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_2 inst_4 _) T
⊢ Triangle.mor₁ (Functor.obj (Functor.mapTriangle (opOp C)) T) ≫
      Iso.hom (Iso.refl (Triangle.obj₂ (Functor.obj (Functor.mapTriangle (opOp C)) T))) =
    Iso.hom (Iso.refl (Triangle.obj₁ (Functor.obj (Functor.mapTriangle (opOp C)) T))) ≫
      (Functor.obj (Equivalence.functor (triangleOpEquivalence Cᵒᵖ))
          (op (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_2 inst_4 _) T
⊢ Triangle.mor₂ (Functor.obj (Functor.mapTriangle (opOp C)) T) ≫
      Iso.hom (Iso.refl (Triangle.obj₃ (Functor.obj (Functor.mapTriangle (opOp C)) T))) =
    Iso.hom (Iso.refl (Triangle.obj₂ (Functor.obj (Functor.mapTriangle (opOp C)) T))) ≫
      (Functor.obj (Equivalence.functor (triangleOpEquivalence Cᵒᵖ))
          (op (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_2 inst_4 _) T
refine :
  (Triangle.mor₃ (Functor.obj (Functor.mapTriangle (opOp C)) T) ≫
        Functor.map (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1)
          (Iso.hom (Iso.refl (Triangle.obj₁ (Functor.obj (Functor.mapTriangle (opOp C)) T))))).unop =
    (Iso.hom (Iso.refl (Triangle.obj₃ (Functor.obj (Functor.mapTriangle (opOp C)) T))) ≫
        (Functor.obj (Equivalence.functor (triangleOpEquivalence Cᵒᵖ))
            (op (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))).mor₃).unop
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖᵒᵖ))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite Cᵒᵖ) ⋯ _) (Functor.obj (Functor.mapTriangle (opOp C)) T)

Tactic:
refine isomorphic_distinguished _ (op_distinguished _ (op_distinguished _ hT)) _
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
      (Quiver.Hom.unop_inj ?_))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.op_distinguished, CategoryTheory.Pretriangulated.Triangle.isoMk, Quiver.Hom.unop_inj, CategoryTheory.Pretriangulated.isomorphic_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_2 inst_4 _) T
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) T.obj₃ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
    (Functor.map (𝟭 C) T.mor₃ ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1) T.mor₃)

Tactic:
have := (shiftFunctorCompIsoId C (-1) 1 (neg_add_cancel 1)).inv.naturality T.mor₃
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_2 inst_4 _) T
this :
  Eq (α :=
    T.obj₃ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)))
    (T.mor₃ ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃))
⊢ Eq.{v_1 + 1} (α :=
    unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (op (op T.obj₁))) ⟶ op T.obj₃)
    (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ 1 (-1) instIsTriangulatedOppositeOpOp._proof_2))
          (op (op T.obj₁))) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C (-1) 1 instIsTriangulatedOppositeOpOp._proof_3)) (op T.obj₁) ≫
        (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁)).op)
    (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ 1 (-1) instIsTriangulatedOppositeOpOp._proof_2))
          (op (op T.obj₁))) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C (-1) 1 instIsTriangulatedOppositeOpOp._proof_3)) (op T.obj₁) ≫
        Quiver.Hom.op
            (CategoryStruct.comp (Y :=
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) T.obj₃))
              (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.obj₃)
              (Functor.map (shiftFunctor C (A := ℤ) 1)
                (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
                  NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁))) ≫
          𝟙 (op T.obj₃))

Tactic:
simp [Functor.map_comp, shift_shiftFunctorCompIsoId_hom_app, ← reassoc_of% this]

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_hom_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
⊢ Equivalence.IsTriangulated.{v_1, u_1, v_1, u_1} (opOpEquivalence C)

Tactic:
.mk'' _ <| inferInstanceAs <| (opOp C).IsTriangulated

Premises used: _private.0.CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence._proof_1, CategoryTheory.Equivalence.IsTriangulated.mk''
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{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
⊢ Functor.IsTriangulated.{v_1, u_1, v_1, u_1} (unopUnop C)

Tactic:
inferInstanceAs ((opOpEquivalence C).functor.IsTriangulated)

Premises used: _private.0.CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop._proof_1
-- 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 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))

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ᵒᵖ
rw :
  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)) ↔
    ∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) T ↔
    ∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

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
T : Triangle.{v_1, u_1} Cᵒᵖ
mp :
  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)) →
    ∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))
mpr :
  (∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op 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))
⊢ 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)) ↔
    ∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
constructor
-- 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ᵒᵖ
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))
⊢ ∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
⟨_, hT, ⟨(triangleOpEquivalence C).counitIso.symm.app T⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Pretriangulated.triangleOpEquivalence, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.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
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))
⊢ ∃ (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} (T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
exact ⟨_, hT, ⟨(triangleOpEquivalence C).counitIso.symm.app T⟩⟩
-- 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ᵒᵖ
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 _) T'
e : T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op 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))

Tactic:
isomorphic_distinguished _ hT' _ ?_

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
T : Triangle.{v_1, u_1} Cᵒᵖ
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 _) T'
e : T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T')
mpr : Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T) ≅ 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))

Tactic:
refine isomorphic_distinguished _ hT' _ ?_

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
T : Triangle.{v_1, u_1} Cᵒᵖ
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 _) T'
e : T ≅ Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T')
⊢ Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T) ≅ T'

Tactic:
exact Iso.unop ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫
      (triangleOpEquivalence C).inverse.mapIso e.symm)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Pretriangulated.triangleOpEquivalence, Opposite.op, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.unop, 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ᵒᵖ
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ)) (distinguishedTriangles C) T₁
T₂ : Triangle.{v_1, u_1} Cᵒᵖ
e : T₂ ≅ T₁
simp :
  ∀
    (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₁))),
    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ᵒᵖ)) (distinguishedTriangles C) T₂

Tactic:
simp only [mem_distinguishedTriangles_iff] at 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ᵒᵖ
e : T₂ ≅ 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₁))
⊢ 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₂))

Tactic:
Pretriangulated.isomorphic_distinguished _ hT₁ _
    ((triangleOpEquivalence C).inverse.mapIso e).unop.symm

Premises used: CategoryTheory.Pretriangulated.triangleOpEquivalence, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.unop, 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₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
e : T₂ ≅ 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₁))
⊢ 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₂))

Tactic:
exact Pretriangulated.isomorphic_distinguished _ hT₁ _
    ((triangleOpEquivalence C).inverse.mapIso e).unop.symm

Premises used: CategoryTheory.Pretriangulated.triangleOpEquivalence, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.unop, 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
X : Cᵒᵖ
dsimp : IsZero.{v_1, u_1} (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))
⊢ IsZero.{v_1, u_1}
    (Triangle.obj₃.{v_1, u_1}
      (Functor.obj (Equivalence.functor (triangleOpEquivalence C))
        (Opposite.op (Triangle.invRotate (contractibleTriangle (Opposite.unop X))))))

Tactic:
dsimp
-- 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))
    (𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))) 0
⊢ IsZero.{v_1, u_1} (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_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ᵒᵖ
change :
  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
⊢ 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))
    (𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0))) 0

Tactic:
change (𝟙 ((0 : C)⟦(-1 : ℤ)⟧)).op = 0

Premises used: Quiver.Hom.op, CategoryTheory.shiftFunctor, CategoryTheory.CategoryStruct.id, OfNat.ofNat, CategoryTheory.Functor.obj, Neg.neg