awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
w : C
w_1 : X₂ ⟶ w
w_2 : w ⟶ 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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk f w_1 w_2)
w_3 : C
w_4 : X₃ ⟶ w_3
w_5 : w_3 ⟶ 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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk g w_4 w_5)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
have octahedron_axiom : ∀ (w : C) (w_6 : X₃ ⟶ w) (w_7 : w ⟶ 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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
      (Triangle.mk (f ≫ g) w_6 w_7)),
  Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
Tactic: obtain ⟨_, _, _, h₁₃'⟩ := distinguished_cocone_triangle (f ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
inst_16 : IsTriangulated.{v_2, u_2} D
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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
have rw : F.map u₁₂ ≫ F.map u₂₃ = F.map (u₁₂ ≫ u₂₃)
Tactic: rw [← comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
inst_16 : IsTriangulated.{v_2, u_2} D
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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
rw : F.map u₁₂ ≫ F.map u₂₃ = F.map (u₁₂ ≫ u₂₃)
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
have rw₁ : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₂ ≫ F.map u₂₃
Tactic: rw [← comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
inst_16 : IsTriangulated.{v_2, u_2} D
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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (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)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
⊢ Nonempty.{v_1 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
have comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
Tactic: have comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃ := by rw [← comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
have rw : ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter 0).retractClosure =
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
Tactic: rw [triangEnvelopeIter, extensionProductIter_zero, retractClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
rw :
  ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter 0).retractClosure =
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
⊢ P.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
have rw₁ : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure =
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
Tactic: rw [triangEnvelopeIter, extensionProductIter_zero, retractClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
rw :
  ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter 0).retractClosure =
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
rw₁ :
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure =
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
⊢ P.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
have rw₂ : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
Tactic: rw [triangEnvelopeIter, extensionProductIter_zero, retractClosure_eq_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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 + 1) =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure
have rw : ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure.extensionProduct
      ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure).retractClosure =
  ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure
Tactic: rw [triangEnvelopeIter, extensionProductIter_succ,
    ← retractClosure_extensionProduct_retractClosure_retractClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
n : ℕ
⊢ P.triangEnvelopeIter (n + 1) =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure
have rw : (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure.extensionProduct
      (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure).retractClosure =
  ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure
Tactic: rw [triangEnvelopeIter, extensionProductIter_succ',
    ← retractClosure_extensionProduct_retractClosure_retractClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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 m : ℕ
h : n ≤ m
⊢ P.triangEnvelopeIter n ≤ P.triangEnvelopeIter m
have h₁ : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
Tactic: apply monotone_retractClosure
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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 m : ℕ
h : n ≤ m
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
have pos : ∀ (hP : P.Nonempty),
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
Tactic: by_cases! hP : P.Nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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 m : ℕ
h : n ≤ m
pos :
  ∀ (hP : P.Nonempty),
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
      (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
have neg : ∀ (hP : P = ⊥),
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
Tactic: by_cases! hP : P.Nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ P.triangEnvelopeIter n
have rw : P.triangEnvelopeIter 0 ≤ P.triangEnvelopeIter n
Tactic: rw [← triangEnvelopeIter_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
⊢ P.triangEnvelope X
have rw : ∀ (hY : ∃ (n : ℕ), P.triangEnvelopeIter n Y), ∃ (n : ℕ), P.triangEnvelopeIter n X
Tactic: rw [prop_triangEnvelope_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n X
have obtain : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n Y), ∃ (n : ℕ), P.triangEnvelopeIter n X
Tactic: obtain ⟨n, hn⟩ := hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (hypothesis)
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
⊢ P.triangEnvelope.shift a X
have hX₁ : ∃ (n : ℕ), P.triangEnvelopeIter n X
Tactic: rw [prop_triangEnvelope_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
⊢ P.triangEnvelope.shift a X
have obtain : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n X), P.triangEnvelope.shift a X
Tactic: obtain ⟨n, hn⟩ := hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
⊢ P.triangEnvelope.shift a X
have rw : ∃ (n : ℕ), P.triangEnvelopeIter n (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)
Tactic: rw [prop_shift_iff, prop_triangEnvelope_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
⊢ P.triangEnvelope.IsTriangulatedClosed₂
have 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₂
Tactic: apply IsTriangulatedClosed₂.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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₃
⊢ P.triangEnvelope T.obj₂
have hP : ∀ (h₁ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₁) (h₂ : ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₃),
  ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
Tactic: rw [prop_triangEnvelope_iff] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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₃
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
have hP : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n T.obj₁), ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
Tactic: obtain ⟨n, hn⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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₁
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
have hP : ∀ (m : ℕ) (hm : P.triangEnvelopeIter m T.obj₃), ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
Tactic: obtain ⟨m, hm⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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₃
⊢ ∃ (n : ℕ), P.triangEnvelopeIter n T.obj₂
have h : P.triangEnvelopeIter (n + (m + 1)) T.obj₂
Tactic: use n + (m + 1)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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 + (m + 1)) T.obj₂
have h : ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m)).retractClosure T.obj₂
Tactic: rw [triangEnvelopeIter_add' P rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
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
have refine : ∀ (h : P ≤ Q), P.triangEnvelope ≤ Q
Tactic: refine ⟨fun h ↦ le_trans P.le_triangEnvelope h, fun h ↦ ?_⟩