-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma distinguished_cocone_triangle {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    ∃ (Z : Cᵒᵖ) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧),
      Triangle.mk f g h ∈ distinguishedTriangles C

Proof state:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop
      ((triangleOpEquivalence C).inverse.obj
        (Triangle.mk f g.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map 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]))

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ (Opposite.unop
          ((triangleOpEquivalence C).inverse.obj
            (Triangle.mk f g.op
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₂ ≫
      (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₃).hom =
    (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₂).hom ≫
      (Triangle.mk g f.unop h).mor₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ (Opposite.unop
          ((triangleOpEquivalence C).inverse.obj
            (Triangle.mk f g.op
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₁ ≫
      (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₂).hom =
    (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₁).hom ≫
      (Triangle.mk g f.unop h).mor₁

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop
      ((triangleOpEquivalence C).inverse.obj
        (Triangle.mk f g.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op))) ∈
    Pretriangulated.distinguishedTriangles

Tactic:
refine Pretriangulated.isomorphic_distinguished _ H _ ?_

Result:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop
      ((triangleOpEquivalence C).inverse.obj
        (Triangle.mk f g.op
          ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op))) ≅
    Triangle.mk g f.unop h

Proof state:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

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

Result:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ Triangle.mk f g.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ 1).map h.op) ∈
    distinguishedTriangles C

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

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

Result:
case intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C