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

Tactic:
rw [mem_distTriang_op_iff']

Premises used: CategoryTheory.Pretriangulated.mem_distTriang_op_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
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) 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}
      (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T) ≅
        Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
⟨T, hT, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro
-- 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 _ _ inst_2 _ inst_3 inst_4 _) 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}
      (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T) ≅
        Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T'))

Tactic:
exact ⟨T, hT, ⟨Iso.refl _⟩⟩
-- 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 _ _ ⋯ _ (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:
hT

Premises used: Set.Mem, setOf, CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles
-- 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 : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
A : Type u_2
inst_6 : Category.{v_2, u_2} A
inst_7 : Abelian.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
inst_8 : F.IsHomological
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
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).op.map F)

Tactic:
F.map_distinguished_exact _ (op_distinguished T hT)

Premises used: Quiver.Hom.op, CategoryTheory.Pretriangulated.op_distinguished, CategoryTheory.ShortComplex.op, CategoryTheory.Functor.map_distinguished_exact, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
-- 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 : IsStableUnderShift.{v_1, u_1, 0} P ℤ
n : ℤ
X : C
hX : P.unop X
⊢ n = - -n

Tactic:
simp
-- 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 : IsStableUnderShift.{v_1, u_1, 0} P ℤ
n : ℤ
X : C
hX : P.unop X
obtain : ∀ (m : ℤ), P.unop.shift (-m) X
⊢ P.unop.shift n X

Tactic:
obtain ⟨m, rfl⟩ : ∃ m, n = -m := ⟨-n , by simp⟩

Premises used: rfl
-- 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 : IsStableUnderShift.{v_1, u_1, 0} P ℤ
X : C
hX : P.unop X
m : ℤ
⊢ P.unop.shift (-m) X

Tactic:
P.le_shift m _ hX

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.ObjectProperty.unop, Int.neg, CategoryTheory.ObjectProperty.le_shift
-- 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 : IsStableUnderShift.{v_1, u_1, 0} P ℤ
X : C
hX : P.unop X
m : ℤ
⊢ P.unop.shift (-m) X

Tactic:
exact P.le_shift m _ hX

Premises used: CategoryTheory.ObjectProperty.le_shift
-- 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.IsTriangulatedClosed₂
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) T
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
⊢ 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:
rw [mem_distTriang_op_iff] at hT

Premises used: CategoryTheory.Pretriangulated.mem_distTriang_op_iff
-- 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.IsTriangulatedClosed₂
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) T
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
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))
⊢ P.op T.obj₁

Tactic:
rw [mem_distTriang_op_iff] at hT

Premises used: CategoryTheory.Pretriangulated.mem_distTriang_op_iff
-- 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.IsTriangulatedClosed₂
T : Triangle.{v_1, u_1} Cᵒᵖ
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) T
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
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))
h₂ : P.op T.obj₁
⊢ P.op T.obj₃

Tactic:
rw [mem_distTriang_op_iff] at hT

Premises used: CategoryTheory.Pretriangulated.mem_distTriang_op_iff
-- 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.IsTriangulatedClosed₂
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))
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
obtain :
  ∀ (X : C) (hX : P X) (e : (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).obj₂ ≅ X),
    isoClosure.{v_1, u_1} P.op T.obj₂
⊢ isoClosure.{v_1, u_1} P.op T.obj₂

Tactic:
obtain ⟨X, hX, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ hT h₃ h₁

Premises used: CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂'
-- 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.IsTriangulatedClosed₂
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))
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
X : C
hX : P X
e : (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).obj₂ ≅ X
⊢ isoClosure.{v_1, u_1} P.op T.obj₂

Tactic:
⟨Opposite.op X, hX, ⟨e.symm.op⟩⟩

Premises used: CategoryTheory.Iso.op, Nonempty.intro, Opposite.op, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm
-- 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.IsTriangulatedClosed₂
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))
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
X : C
hX : P X
e : (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T)).obj₂ ≅ X
⊢ isoClosure.{v_1, u_1} P.op T.obj₂

Tactic:
exact ⟨Opposite.op X, hX, ⟨e.symm.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 : IsTriangulatedClosed₂.{v_1, u_1} P
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
h₁ : P.unop T.obj₁
h₃ : P.unop T.obj₃
obtain :
  ∀ (X : Cᵒᵖ) (hX : P X) (e : (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T)).obj₂ ≅ X),
    P.unop.isoClosure T.obj₂
⊢ P.unop.isoClosure T.obj₂

Tactic:
obtain ⟨X, hX, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ (op_distinguished _ hT) h₃ h₁

Premises used: CategoryTheory.Pretriangulated.op_distinguished, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂'
-- 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 : IsTriangulatedClosed₂.{v_1, u_1} P
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
h₁ : P.unop T.obj₁
h₃ : P.unop T.obj₃
X : Cᵒᵖ
hX : P X
e : (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T)).obj₂ ≅ X
⊢ P.unop.isoClosure T.obj₂

Tactic:
⟨Opposite.unop X, hX, ⟨e.symm.unop⟩⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm, Opposite.unop, CategoryTheory.Iso.unop
-- 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 : IsTriangulatedClosed₂.{v_1, u_1} P
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
h₁ : P.unop T.obj₁
h₃ : P.unop T.obj₃
X : Cᵒᵖ
hX : P X
e : (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (Opposite.op T)).obj₂ ≅ X
⊢ P.unop.isoClosure T.obj₂

Tactic:
exact ⟨Opposite.unop X, hX, ⟨e.symm.unop⟩⟩
-- 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
hf : trW.{v_1, u_1} P.op (X := Opposite.op Y) (Y := Opposite.op X) f.op
obtain :
  ∀ (Z : Cᵒᵖ) (a : Opposite.op X ⟶ Z)
    (b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op Y))
    (h₁ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
        (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f.op a b))
    (h₂ : P.op Z), P.trW f
⊢ P.trW f

Tactic:
obtain ⟨Z, a, b, h₁, h₂⟩ := hf
-- 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
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op Y)
h₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f.op a b)
h₂ : P.op Z
rw :
  ∃ (X_1 : C) (f_1 : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f_1 f h)),
    P X_1
⊢ P.trW f

Tactic:
rw [ObjectProperty.trW_iff']

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- 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
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op Y)
h₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f.op a b)
h₂ : P.op Z
⊢ ∃ (X_1 : C) (f_1 : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f_1 f h)),
    P X_1

Tactic:
⟨_, _, _, Pretriangulated.unop_distinguished _ h₁, h₂⟩

Premises used: CategoryTheory.Pretriangulated.unop_distinguished, Exists.intro
-- 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
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op Y)
h₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f.op a b)
h₂ : P.op Z
⊢ ∃ (X_1 : C) (f_1 : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f_1 f h)),
    P X_1

Tactic:
exact ⟨_, _, _, Pretriangulated.unop_distinguished _ h₁, h₂⟩
-- 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 : ObjectProperty.IsTriangulated.{v_1, u_1} P
X Y : Cᵒᵖ
f : X ⟶ Y
hf : P.unop.trW f.unop
obtain :
  ∀ (Z : C) (a : Opposite.unop X ⟶ Z)
    (b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Y))
    (h₁ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f.unop a b))
    (h₂ : P.unop Z), trW.{v_1, u_1} P (X := X) (Y := Y) f
⊢ trW.{v_1, u_1} P (X := X) (Y := Y) f

Tactic:
obtain ⟨Z, a, b, h₁, h₂⟩ := hf
-- 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 : ObjectProperty.IsTriangulated.{v_1, u_1} P
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Y)
h₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f.unop a b)
h₂ : P.unop Z
rw :
  ∃ (X_1 : Cᵒᵖ) (f_1 : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
      (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f_1 f h)),
    P X_1
⊢ trW.{v_1, u_1} P (X := X) (Y := Y) f

Tactic:
rw [ObjectProperty.trW_iff']

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- 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 : ObjectProperty.IsTriangulated.{v_1, u_1} P
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Y)
h₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f.unop a b)
h₂ : P.unop Z
⊢ ∃ (X_1 : Cᵒᵖ) (f_1 : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
      (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f_1 f h)),
    P X_1

Tactic:
⟨_, _, _, Pretriangulated.op_distinguished _ h₁, h₂⟩

Premises used: CategoryTheory.Pretriangulated.op_distinguished, Exists.intro
-- 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 : ObjectProperty.IsTriangulated.{v_1, u_1} P
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Y)
h₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _) (Triangle.mk f.unop a b)
h₂ : P.unop Z
⊢ ∃ (X_1 : Cᵒᵖ) (f_1 : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
      (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk f_1 f h)),
    P X_1

Tactic:
exact ⟨_, _, _, Pretriangulated.op_distinguished _ h₁, h₂⟩