awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
⊢ P.retractClosure.extensionProductIter 0 ≤ (P.extensionProductIter 0).retractClosure

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
H : P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
succ :
  P.retractClosure.extensionProduct (P.retractClosure.extensionProductIter n) ≤
    (P.extensionProductIter (n + 1)).retractClosure
succ₁ :
  P.retractClosure.extensionProduct (P.retractClosure.extensionProductIter n) ≤
    (P.extensionProduct (P.extensionProductIter n)).retractClosure
succ₂ :
  P.retractClosure.extensionProduct (P.extensionProductIter n).retractClosure ≤
    (P.extensionProduct (P.extensionProductIter n)).retractClosure
succ₃ succ₄ :
  (P.extensionProduct (P.extensionProductIter n)).retractClosure ≤
    (P.extensionProduct (P.extensionProductIter n)).retractClosure
⊢ P.retractClosure.extensionProductIter (n + 1) ≤ (P.extensionProductIter (n + 1)).retractClosure

Tactic:
grw [extensionProductIter_succ, extensionProductIter_succ, monotone_extensionProduct_right _ H,
      extensionProduct_retractClosure_retractClosure_le]

Premises used: CategoryTheory.ObjectProperty.monotone_extensionProduct_right, CategoryTheory.ObjectProperty.extensionProductIter_succ, CategoryTheory.ObjectProperty.extensionProduct_retractClosure_retractClosure_le
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
zero : P.retractClosure.extensionProductIter 0 ≤ (P.extensionProductIter 0).retractClosure
succ :
  ∀ (n : ℕ) (H : P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure),
    P.retractClosure.extensionProductIter (n + 1) ≤ (P.extensionProductIter (n + 1)).retractClosure
⊢ P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure

Tactic:
induction n with
  | zero => simp
  | succ n H =>
    grw [extensionProductIter_succ, extensionProductIter_succ, monotone_extensionProduct_right _ H,
      extensionProduct_retractClosure_retractClosure_le]

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_succ, CategoryTheory.ObjectProperty.extensionProduct_retractClosure_retractClosure_le
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
a : (P.retractClosure.extensionProductIter n).retractClosure ≤ (P.extensionProductIter n).retractClosure
a₁ : (P.extensionProductIter n).retractClosure ≤ (P.retractClosure.extensionProductIter n).retractClosure
⊢ (P.retractClosure.extensionProductIter n).retractClosure = (P.extensionProductIter n).retractClosure

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
a : P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
⊢ (P.retractClosure.extensionProductIter n).retractClosure ≤ (P.extensionProductIter n).retractClosure

Tactic:
rw [retractClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.retractClosure_le_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
⊢ P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure

Tactic:
extensionProductIter_retractClosure_le P

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_retractClosure_le
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
⊢ P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure

Tactic:
exact extensionProductIter_retractClosure_le P

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_retractClosure_le
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
⊢ (P.extensionProductIter n).retractClosure ≤ (P.retractClosure.extensionProductIter n).retractClosure

Tactic:
monotone_retractClosure (monotone_extensionProductIter (le_retractClosure P) n)

Premises used: CategoryTheory.ObjectProperty.monotone_retractClosure, CategoryTheory.ObjectProperty.monotone_extensionProductIter, CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
n : ℕ
⊢ (P.extensionProductIter n).retractClosure ≤ (P.retractClosure.extensionProductIter n).retractClosure

Tactic:
exact monotone_retractClosure (monotone_extensionProductIter (le_retractClosure P) n)

Premises used: CategoryTheory.ObjectProperty.monotone_retractClosure, CategoryTheory.ObjectProperty.monotone_extensionProductIter, CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
⊢ P.trW f ↔
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)),
      P Z

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
mp :
  (∃ (Z_1 : C) (g_1 : Z ⟶ Z_1) (h : Z_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g g_1 h)),
      P Z_1) →
    ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)),
      P X
mpr :
  (∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)),
      P X) →
    ∃ (Z_1 : C) (g_1 : Z ⟶ Z_1) (h : Z_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g g_1 h)),
      P Z_1
⊢ (∃ (Z_1 : C) (g_1 : Z ⟶ Z_1) (h : Z_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g g_1 h)),
      P Z_1) ↔
    ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)),
      P X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
Y Z_1 : C
g_1 : Y ⟶ Z_1
Z : C
g : Z_1 ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g_1 g h)
mem : P Z
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g_1 h)),
    P X

Tactic:
⟨_, _, _, inv_rot_of_distTriang _ H, P.le_shift (-1) _ mem⟩

Premises used: CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Exists.intro, OfNat.ofNat, Neg.neg, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
Y Z_1 : C
g_1 : Y ⟶ Z_1
Z : C
g : Z_1 ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g_1 g h)
mem : P Z
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g_1 h)),
    P X

Tactic:
exact ⟨_, _, _, inv_rot_of_distTriang _ H, P.le_shift (-1) _ mem⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
Y Z_1 : C
g_1 : Y ⟶ Z_1
Z : C
g : Z ⟶ Y
h : Z_1 ⟶ 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)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g g_1 h)
mem : P Z
⊢ ∃ (Z : C) (g : Z_1 ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk g_1 g h)),
    P Z

Tactic:
⟨_, _, _, rot_of_distTriang _ H, P.le_shift 1 _ mem⟩

Premises used: Exists.intro, CategoryTheory.Pretriangulated.rot_of_distTriang, OfNat.ofNat, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
Y Z_1 : C
g_1 : Y ⟶ Z_1
Z : C
g : Z ⟶ Y
h : Z_1 ⟶ 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)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g g_1 h)
mem : P Z
⊢ ∃ (Z : C) (g : Z_1 ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk g_1 g h)),
    P Z

Tactic:
exact ⟨_, _, _, rot_of_distTriang _ H, P.le_shift 1 _ mem⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : P T.obj₃
⊢ P.trW T.mor₁

Tactic:
⟨_, _, _, hT, h⟩

Premises used: CategoryTheory.ObjectProperty.trW, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : P T.obj₁
rw :
  ∃ (X : C) (f : X ⟶ T.obj₂) (h : T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f T.mor₂ h)),
    P X
⊢ P.trW T.mor₂

Tactic:
rw [trW_iff']

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : P T.obj₁
⊢ ∃ (X : C) (f : X ⟶ T.obj₂) (h : T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f T.mor₂ h)),
    P X

Tactic:
⟨_, _, _, hT, h⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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.IsStableUnderShift ℤ
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : P T.obj₁
⊢ ∃ (X : C) (f : X ⟶ T.obj₂) (h : T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f T.mor₂ h)),
    P X

Tactic:
exact ⟨_, _, _, hT, h⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.isoClosure.trW f ↔ P.trW f
⊢ P.isoClosure.trW = P.trW

Tactic:
ext X Y f
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
h : P.isoClosure.trW f → P.trW f
h₁ : P.trW f → P.isoClosure.trW f
⊢ P.isoClosure.trW f ↔ P.trW f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ P.trW f

Tactic:
⟨Z', g ≫ e.hom, e.inv ≫ h, isomorphic_distinguished _ mem _ ?_, hZ'⟩

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.ObjectProperty.trW, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
Z' : C
hZ' : P Z'
e : Z ≅ Z'
h₁ : Triangle.mk f (g ≫ e.hom) (e.inv ≫ h) ≅ Triangle.mk f g h
⊢ P.trW f

Tactic:
refine ⟨Z', g ≫ e.hom, e.inv ≫ h, isomorphic_distinguished _ mem _ ?_, hZ'⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Triangle.mk f (g ≫ e.hom) (e.inv ≫ h) ≅ Triangle.mk f g h

Tactic:
exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hZ : P Z
⊢ P.isoClosure.trW f

Tactic:
⟨Z, g, h, mem, ObjectProperty.le_isoClosure _ _ hZ⟩

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.trW, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hZ : P Z
⊢ P.isoClosure.trW f

Tactic:
exact ⟨Z, g, h, mem, ObjectProperty.le_isoClosure _ _ hZ⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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 Q : ObjectProperty.{v_1, u_1} C
h : P ≤ Q
X Y : C
f : X ⟶ Y
hf : P.trW f
⊢ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)),
    P Z

Tactic:
rw [trW_iff] at hf ⊢

Premises used: CategoryTheory.ObjectProperty.trW_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} 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 Q : ObjectProperty.{v_1, u_1} C
h : P ≤ Q
X Y : C
f : X ⟶ Y
hf :
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)),
    P Z
obtain :
  ∀ (Z : C) (a : Y ⟶ Z) (b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f a b))
    (hZ : P Z),
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)),
      Q Z
⊢ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)),
    Q Z

Tactic:
obtain ⟨Z, a, b, hT, hZ⟩ := hf