awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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.triangEnvelopeIter 0 ≤ P.triangEnvelopeIter n

Tactic:
exact P.monotone'_triangEnvelopeIter (Nat.zero_le n)

Premises used: Nat.zero_le, CategoryTheory.ObjectProperty.monotone'_triangEnvelopeIter
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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.IsStrongTriangulatedGenerator ↔ ∃ (n : ℕ), P.triangEnvelopeIter n = ⊤

Tactic:
Iff.rfl

Premises used: CategoryTheory.ObjectProperty.IsStrongTriangulatedGenerator, Iff.rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : C
⊢ P.triangEnvelope X ↔ ∃ (n : ℕ), P.triangEnvelopeIter n X

Tactic:
prop_iSup_iff _ X

Premises used: CategoryTheory.ObjectProperty.triangEnvelope, CategoryTheory.ObjectProperty.prop_iSup_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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.triangEnvelopeIter n ≤ P.triangEnvelope

Tactic:
le_iSup _ _

Premises used: le_iSup, CategoryTheory.ObjectProperty.triangEnvelope
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 ≤ P.triangEnvelope

Tactic:
(P.le_triangEnvelopeIter 0).trans (P.triangEnvelopeIter_le_triangEnvelope 0)

Premises used: CategoryTheory.ObjectProperty.triangEnvelopeIter_le_triangEnvelope, LE.le.trans, OfNat.ofNat, CategoryTheory.ObjectProperty.le_triangEnvelopeIter
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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.Nonempty
⊢ P.triangEnvelope.Nonempty

Tactic:
.mono P.le_triangEnvelope

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, CategoryTheory.ObjectProperty.le_triangEnvelope
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
⊢ P.triangEnvelope ≤ Q.triangEnvelope

Tactic:
iSup_le fun n => (P.monotone_triangEnvelopeIter h n).trans
    (Q.triangEnvelopeIter_le_triangEnvelope n)

Premises used: CategoryTheory.ObjectProperty.triangEnvelopeIter_le_triangEnvelope, CategoryTheory.ObjectProperty.triangEnvelope, CategoryTheory.ObjectProperty.monotone_triangEnvelopeIter, iSup_le, LE.le.trans
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
r : Retract X Y
hY : P.triangEnvelope Y
rw : ∀ (hY : ∃ (n : ℕ), P.triangEnvelopeIter n Y), ∃ (n : ℕ), P.triangEnvelopeIter n X
⊢ P.triangEnvelope X

Tactic:
rw [prop_triangEnvelope_iff] at hY ⊢

Premises used: CategoryTheory.ObjectProperty.prop_triangEnvelope_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
r : Retract X Y
hY : ∃ (n : ℕ), P.triangEnvelopeIter n Y
obtain : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n Y), ∃ (n : ℕ), P.triangEnvelopeIter n X
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n X

Tactic:
obtain ⟨n, hn⟩ := hY
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
r : Retract X Y
n : ℕ
hn : P.triangEnvelopeIter n Y
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n X

Tactic:
⟨n, IsStableUnderRetracts.of_retract r hn⟩

Premises used: CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_retract, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
r : Retract X Y
n : ℕ
hn : P.triangEnvelopeIter n Y
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n X

Tactic:
exact ⟨n, IsStableUnderRetracts.of_retract r hn⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
a : ℤ
X : C
hX : P.triangEnvelope X
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n X

Tactic:
rw [prop_triangEnvelope_iff] at hX

Premises used: CategoryTheory.ObjectProperty.prop_triangEnvelope_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
a : ℤ
X : C
hX : ∃ (n : ℕ), P.triangEnvelopeIter n X
obtain : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n X), P.triangEnvelope.shift a X
⊢ P.triangEnvelope.shift a X

Tactic:
obtain ⟨n, hn⟩ := hX
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
rw : ∃ (n : ℕ), P.triangEnvelopeIter n (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)
⊢ P.triangEnvelope.shift a X

Tactic:
rw [prop_shift_iff, prop_triangEnvelope_iff]

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff, CategoryTheory.ObjectProperty.prop_triangEnvelope_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)

Tactic:
⟨n, IsStableUnderShiftBy.le_shift _ hn⟩

Premises used: CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)

Tactic:
exact ⟨n, IsStableUnderShiftBy.le_shift _ hn⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{v_1, u_1} C
hP :
  ∀ (T : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
      P.triangEnvelope T.obj₁ → P.triangEnvelope T.obj₃ → P.triangEnvelope T.obj₂
⊢ P.triangEnvelope.IsTriangulatedClosed₂

Tactic:
apply IsTriangulatedClosed₂.mk'

Premises used: CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk'
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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.triangEnvelope T.obj₁
h₂ : P.triangEnvelope T.obj₃
hP :
  ∀ (h₁ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₁) (h₂ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₃),
    ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
⊢ P.triangEnvelope T.obj₂

Tactic:
rw [prop_triangEnvelope_iff] at h₁ h₂ ⊢

Premises used: CategoryTheory.ObjectProperty.prop_triangEnvelope_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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₁ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₁
h₂ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₃
hP : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n T.obj₁), ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂

Tactic:
obtain ⟨n, hn⟩ := h₁
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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₂ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₃
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
hP : ∀ (m : ℕ) (hm : P.triangEnvelopeIter m T.obj₃), ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂

Tactic:
obtain ⟨m, hm⟩ := h₂
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
h : P.triangEnvelopeIter (n + (m + 1)) T.obj₂
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂

Tactic:
use n + (m + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
h : ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂
⊢ P.triangEnvelopeIter (n + (m + 1)) T.obj₂

Tactic:
rw [triangEnvelopeIter_add' P rfl]

Premises used: CategoryTheory.ObjectProperty.triangEnvelopeIter_add', rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
⊢ ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂

Tactic:
le_retractClosure _ _ ⟨_, _, _, _, _, hT, hn, hm⟩

Premises used: And.intro, Exists.intro, CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : IsTriangulated.{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
n : ℕ
hn : P.triangEnvelopeIter n T.obj₁
m : ℕ
hm : P.triangEnvelopeIter m T.obj₃
⊢ ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂

Tactic:
exact le_retractClosure _ _ ⟨_, _, _, _, _, hT, hn, hm⟩

Premises used: CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
⊢ P.triangEnvelope ≤ Q ↔ P ≤ Q

Tactic:
⟨fun h ↦ le_trans P.le_triangEnvelope h, fun h ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.le_triangEnvelope, Iff.intro, le_trans
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
refine : ∀ (h : P ≤ Q), P.triangEnvelope ≤ Q
⊢ P.triangEnvelope ≤ Q ↔ P ≤ Q

Tactic:
refine ⟨fun h ↦ le_trans P.le_triangEnvelope h, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
rw : ∀ (i : ℕ), P.triangEnvelopeIter i ≤ Q
⊢ P.triangEnvelope ≤ Q

Tactic:
rw [triangEnvelope, iSup_le_iff]

Premises used: CategoryTheory.ObjectProperty.triangEnvelope, iSup_le_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
rw : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q
⊢ P.triangEnvelopeIter n ≤ Q

Tactic:
rw [triangEnvelopeIter, retractClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.retractClosure_le_iff, CategoryTheory.ObjectProperty.triangEnvelopeIter
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
h₁ : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ Q
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q

Tactic:
apply extensionProductIter_le_of_isTriangulatedClosed₂

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_le_of_isTriangulatedClosed₂
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
h₁ : (P.shiftClosure ℤ).binaryProductsClosure ≤ Q
h₂ : P.shiftClosure ℤ ≤ Q
h₃ h₄ h₅ h₆ : P ≤ Q
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ Q

Tactic:
rwa [retractClosure_le_iff, binaryProductsClosure_le_iff, shiftClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.binaryProductsClosure_le_iff, CategoryTheory.ObjectProperty.shiftClosure_le_iff, CategoryTheory.ObjectProperty.retractClosure_le_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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.IsClassicalTriangulatedGenerator ↔ P.triangEnvelope = ⊤

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : P.IsStrongTriangulatedGenerator
obtain : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n = ⊤), P.IsClassicalTriangulatedGenerator
⊢ P.IsClassicalTriangulatedGenerator

Tactic:
obtain ⟨n, hn⟩ := h
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : ℕ
hn : P.triangEnvelopeIter n = ⊤
rw : ⊤ ≤ P.triangEnvelope
⊢ P.IsClassicalTriangulatedGenerator

Tactic:
rw [isClassicalTriangulatedGenerator_iff, eq_top_iff]

Premises used: eq_top_iff, CategoryTheory.ObjectProperty.isClassicalTriangulatedGenerator_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : ℕ
hn : P.triangEnvelopeIter n = ⊤
⊢ ⊤ ≤ P.triangEnvelope

Tactic:
hn ▸ (P.triangEnvelopeIter_le_triangEnvelope n)

Premises used: CategoryTheory.ObjectProperty.triangEnvelopeIter_le_triangEnvelope, Eq.rec
-- Module: Mathlib.CategoryTheory.Triangulated.Generators
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 : ℕ
hn : P.triangEnvelopeIter n = ⊤
⊢ ⊤ ≤ P.triangEnvelope

Tactic:
exact hn ▸ (P.triangEnvelopeIter_le_triangEnvelope n)
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : F.ShiftSequence ℤ
X : C
⊢ F.homologicalKernel X ↔ ∀ (n : ℤ), IsZero.{v_3, u_3} ((F.shift n).obj X)

Tactic:
simp only [← fun (n : ℤ) => Iso.isZero_iff ((F.isoShift n).app X),
    homologicalKernel, comp_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.homologicalKernel, CategoryTheory.Functor.isoShift, CategoryTheory.Iso.isZero_iff, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _) T
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)

Tactic:
IsHomological.exact _ hT

Premises used: CategoryTheory.Functor.IsHomological.exact