awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ trW.{v_1, u_1} P.op (X := X) (Y := Y) f ↔ P.trW f.unop

Tactic:
⟨P.trW_of_op, P.op.trW_of_unop⟩

Premises used: CategoryTheory.ObjectProperty.trW_of_unop, CategoryTheory.ObjectProperty.trW_of_op, Iff.intro, CategoryTheory.ObjectProperty.op
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), P.op.trW f ↔ P.trW.op f
⊢ P.op.trW = P.trW.op

Tactic:
ext X Y f
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.op.trW f ↔ P.trW.op f

Tactic:
P.trW_op_iff

Premises used: CategoryTheory.ObjectProperty.trW_op_iff, CategoryTheory.MorphismProperty.op, CategoryTheory.ObjectProperty.trW
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.op.trW f ↔ P.trW.op f

Tactic:
exact P.trW_op_iff

Premises used: CategoryTheory.ObjectProperty.trW_op_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : (Triangle.{v_1, u_1} C)ᵒᵖ
⊢ Triangle.mor₁
        (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
          (CategoryStruct.comp (Y :=
            Opposite.unop
              (Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C 1))
                (Functor.obj (functor C) T).obj₁))
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                (Functor.obj (functor C) T).obj₁))
            (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂
            (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
              (CategoryStruct.comp (Y :=
                Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1}
                    (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                      Equivalence.inverse (opShiftFunctorEquivalence C 1))
                    (Functor.obj (functor C) T).obj₁))
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                    (Functor.obj (functor C) T).obj₁))
                (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₁
            (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
              (CategoryStruct.comp (Y :=
                Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1}
                    (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                      Equivalence.inverse (opShiftFunctorEquivalence C 1))
                    (Functor.obj (functor C) T).obj₁))
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                    (Functor.obj (functor C) T).obj₁))
                (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))))) ≫
      (Opposite.unop T).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : (Triangle.{v_1, u_1} C)ᵒᵖ
⊢ Triangle.mor₂
        (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
          (CategoryStruct.comp (Y :=
            Opposite.unop
              (Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C 1))
                (Functor.obj (functor C) T).obj₁))
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                (Functor.obj (functor C) T).obj₁))
            (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₃
            (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
              (CategoryStruct.comp (Y :=
                Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1}
                    (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                      Equivalence.inverse (opShiftFunctorEquivalence C 1))
                    (Functor.obj (functor C) T).obj₁))
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                    (Functor.obj (functor C) T).obj₁))
                (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₂
            (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
              (CategoryStruct.comp (Y :=
                Opposite.unop
                  (Functor.obj.{v_1, v_1, u_1, u_1}
                    (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                      Equivalence.inverse (opShiftFunctorEquivalence C 1))
                    (Functor.obj (functor C) T).obj₁))
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                    (Functor.obj (functor C) T).obj₁))
                (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))))) ≫
      (Opposite.unop T).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : (Triangle.{v_1, u_1} C)ᵒᵖ
⊢ (Triangle.mor₃
          (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
            (CategoryStruct.comp (Y :=
              Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1}
                  (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                    Equivalence.inverse (opShiftFunctorEquivalence C 1))
                  (Functor.obj (functor C) T).obj₁))
              (Quiver.Hom.unop
                (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                  (Functor.obj (functor C) T).obj₁))
              (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1)
          (Iso.hom
            (Iso.refl
              (Triangle.obj₁
                (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
                  (CategoryStruct.comp (Y :=
                    Opposite.unop
                      (Functor.obj.{v_1, v_1, u_1, u_1}
                        (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                          Equivalence.inverse (opShiftFunctorEquivalence C 1))
                        (Functor.obj (functor C) T).obj₁))
                    (Quiver.Hom.unop
                      (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                        (Functor.obj (functor C) T).obj₁))
                    (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))))))).op =
    (Iso.hom
          (Iso.refl
            (Triangle.obj₃
              (Triangle.mk (Functor.obj (functor C) T).mor₂.unop (Functor.obj (functor C) T).mor₁.unop
                (CategoryStruct.comp (Y :=
                  Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1}
                      (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                        Equivalence.inverse (opShiftFunctorEquivalence C 1))
                      (Functor.obj (functor C) T).obj₁))
                  (Quiver.Hom.unop
                    (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                      (Functor.obj (functor C) T).obj₁))
                  (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.obj (functor C) T).mor₃.unop))))) ≫
        (Opposite.unop T).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.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
refine_1 :
  (Functor.obj (inverse C ⋙ functor C) T).mor₁ ≫ Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₂) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₁) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₁
refine_2 :
  (Functor.obj (inverse C ⋙ functor C) T).mor₂ ≫ Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₃) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₂) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₂
refine_3 :
  (Functor.obj (inverse C ⋙ functor C) T).mor₃ ≫
      Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₁)) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₃) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₃
⊢ Functor.obj (inverse C ⋙ functor C) T ≅ Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ (Functor.obj (inverse C ⋙ functor C) T).mor₁ ≫ Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₂) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₁) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ (Functor.obj (inverse C ⋙ functor C) T).mor₂ ≫ Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₃) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₂) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
refine_3 :
  CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))))
          (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) T.obj₃ :
            Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₃ ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                T.obj₃)
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) T.mor₃.unop) ≫
                NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T.obj₁) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁) :
        T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
      (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (𝟙 T.obj₁) :
        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) T.obj₁) =
    𝟙 T.obj₃ ≫ T.mor₃
⊢ (Functor.obj (inverse C ⋙ functor C) T).mor₃ ≫
      Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₁)) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₃) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
refine_3 :
  T.mor₃ ≫
      𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₁)) =
    T.mor₃
⊢ CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))))
          (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) T.obj₃ :
            Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₃ ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                T.obj₃)
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) T.mor₃.unop) ≫
                NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T.obj₁) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁) :
        T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
      (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (𝟙 T.obj₁) :
        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) T.obj₁) =
    𝟙 T.obj₃ ≫ T.mor₃

Tactic:
rw [Functor.map_id, comp_id, id_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc,
        opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp,
        Iso.hom_inv_id_app, Functor.map_id]

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ T.mor₃ ≫
      𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₁)) =
    T.mor₃

Tactic:
simp only [Functor.id_obj, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
⊢ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁.unop ≫ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁.unop = (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁.unop

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ Nonempty.{v_1 + 1} (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
⟨o.m₃.op, o.m₁.op, congr($(o.comm₄).op), ?_, congr($(o.comm₁).op), ?_, ?_⟩

Premises used: CategoryTheory.Triangulated.Octahedron.mk, CategoryTheory.Triangulated.Octahedron'.m₁, congrArg, Quiver.Hom.op, id, CategoryTheory.Triangulated.Octahedron'.m₃, CategoryTheory.Triangulated.Octahedron'.comm₄, Nonempty.intro, CategoryTheory.Triangulated.Octahedron'.comm₁
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated
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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : 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ᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
refine_1 : o.m₃.op ≫ w₁₃ = w₁₂
refine_2 : w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃
refine_3 :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    (Triangle.mk o.m₃.op o.m₁.op (w₂₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) v₁₂))
⊢ Nonempty.{v_1 + 1} (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
refine ⟨o.m₃.op, o.m₁.op, congr($(o.comm₄).op), ?_, congr($(o.comm₁).op), ?_, ?_⟩