awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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₁₃)
comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
H : Octahedron comm' (w₁₂ :=
  F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁)
  ⋯ (w₂₃ :=
  F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁)
  ⋯ (w₁₃ :=
  F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁)
  ⋯ :=
  someOctahedron comm' ⋯ ⋯ ⋯
⊢ F.map (v₁₂ ≫ F.preimage H.m₁) = F.map (u₂₃ ≫ v₁₃)

Tactic:
simpa using H.comm₁

Premises used: CategoryTheory.Triangulated.Octahedron.comm₁
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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₁₃)
comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
H : Octahedron comm' (w₁₂ :=
  F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁)
  ⋯ (w₂₃ :=
  F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁)
  ⋯ (w₁₃ :=
  F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁)
  ⋯ :=
  someOctahedron comm' ⋯ ⋯ ⋯
⊢ F.map (F.preimage H.m₁ ≫ w₁₃) = F.map w₁₂

Tactic:
simpa [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app X₁)] using H.comm₂

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Triangulated.Octahedron.comm₂, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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₁₃)
comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
H : Octahedron comm' (w₁₂ :=
  F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁)
  ⋯ (w₂₃ :=
  F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁)
  ⋯ (w₁₃ :=
  F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁)
  ⋯ :=
  someOctahedron comm' ⋯ ⋯ ⋯
⊢ F.map (v₁₃ ≫ F.preimage H.m₃) = F.map v₂₃

Tactic:
simpa using H.comm₃

Premises used: CategoryTheory.Triangulated.Octahedron.comm₃
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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₁₃)
comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
H : Octahedron comm' (w₁₂ :=
  F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁)
  ⋯ (w₂₃ :=
  F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁)
  ⋯ (w₁₃ :=
  F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁)
  ⋯ :=
  someOctahedron comm' ⋯ ⋯ ⋯
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk (F.preimage H.m₁) (F.preimage H.m₃) (w₂₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂))

Tactic:
simpa [← F.map_distinguished_iff] using H.mem

Premises used: CategoryTheory.Triangulated.Octahedron.mem, CategoryTheory.Functor.map_distinguished_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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₁₃)
comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
H : Octahedron comm' (w₁₂ :=
  F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁)
  ⋯ (w₂₃ :=
  F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁)
  ⋯ (w₁₃ :=
  F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁)
  ⋯ :=
  someOctahedron comm' ⋯ ⋯ ⋯
⊢ Nonempty.{v_1 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
exact
      ⟨{m₁ := F.preimage H.m₁
        m₃ := F.preimage H.m₃
        comm₁ := F.map_injective (by simpa using H.comm₁)
        comm₂ := F.map_injective (by
          simpa [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app X₁)] using H.comm₂)
        comm₃ := F.map_injective (by simpa using H.comm₃)
        comm₄ := F.map_injective (by
          simpa [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app X₂)] using H.comm₄)
        mem := by simpa [← F.map_distinguished_iff] using H.mem }⟩
-- 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
rw :
  ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter 0).retractClosure =
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
rw₁ :
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure =
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
rw₂ rw₃ :
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
⊢ P.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure

Tactic:
rw [triangEnvelopeIter, extensionProductIter_zero, retractClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.retractClosure_eq_self, CategoryTheory.ObjectProperty.triangEnvelopeIter, CategoryTheory.ObjectProperty.extensionProductIter_zero
-- 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 : ℕ
rw :
  ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure.extensionProduct
        ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter
            n).retractClosure).retractClosure =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure
⊢ P.triangEnvelopeIter (n + 1) =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure

Tactic:
rw [triangEnvelopeIter, extensionProductIter_succ,
    ← retractClosure_extensionProduct_retractClosure_retractClosure]

Premises used: CategoryTheory.ObjectProperty.retractClosure_extensionProduct_retractClosure_retractClosure, CategoryTheory.ObjectProperty.extensionProductIter_succ, 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 : ObjectProperty.{v_1, u_1} C
n : ℕ
⊢ ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure.extensionProduct
        ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter
            n).retractClosure).retractClosure =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure

Tactic:
simp
-- 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
n : ℕ
rw :
  (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure.extensionProduct
        (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure
⊢ P.triangEnvelopeIter (n + 1) =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure

Tactic:
rw [triangEnvelopeIter, extensionProductIter_succ',
    ← retractClosure_extensionProduct_retractClosure_retractClosure]

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_succ', CategoryTheory.ObjectProperty.retractClosure_extensionProduct_retractClosure_retractClosure, 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 : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n : ℕ
⊢ (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure.extensionProduct
        (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure

Tactic:
simp
-- 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
n m n' : ℕ
h : n = n' + 1
⊢ P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n').extensionProduct (P.triangEnvelopeIter m)).retractClosure

Tactic:
simp only [triangEnvelopeIter, retractClosure_extensionProduct_retractClosure_retractClosure,
    extensionProductIter_add _ h]

Premises used: CategoryTheory.ObjectProperty.retractClosure_extensionProduct_retractClosure_retractClosure, CategoryTheory.ObjectProperty.extensionProductIter_add, 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 : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n m m' : ℕ
h : m = m' + 1
⊢ P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m')).retractClosure

Tactic:
simp only [triangEnvelopeIter, retractClosure_extensionProduct_retractClosure_retractClosure,
    extensionProductIter_add' _ h]

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_add', CategoryTheory.ObjectProperty.retractClosure_extensionProduct_retractClosure_retractClosure, 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
hPQ : P ≤ Q
n : ℕ
⊢ P.triangEnvelopeIter n ≤ Q.triangEnvelopeIter n

Tactic:
monotone_retractClosure <| monotone_extensionProductIter
    (monotone_retractClosure <| limitsClosure_monotone _ <| monotone_shiftClosure hPQ) n

Premises used: CategoryTheory.ObjectProperty.monotone_retractClosure, CategoryTheory.ObjectProperty.monotone_shiftClosure, CategoryTheory.ObjectProperty.monotone_extensionProductIter, CategoryTheory.ObjectProperty.limitsClosure_monotone
-- 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 m : ℕ
h : n ≤ m
h₁ :
  (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
⊢ P.triangEnvelopeIter n ≤ P.triangEnvelopeIter m

Tactic:
apply monotone_retractClosure

Premises used: CategoryTheory.ObjectProperty.monotone_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
n m : ℕ
h : n ≤ m
pos :
  ∀ (hP : P.Nonempty),
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
      (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
neg :
  ∀ (hP : P = ⊥),
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
      (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

Tactic:
by_cases! hP : P.Nonempty

Premises used: CategoryTheory.ObjectProperty.Nonempty
-- 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 m : ℕ
h : n ≤ m
hP : P.Nonempty
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

Tactic:
monotone'_extensionProductIter _ h

Premises used: CategoryTheory.ObjectProperty.monotone'_extensionProductIter
-- 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 m : ℕ
h : n ≤ m
hP : P.Nonempty
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

Tactic:
exact monotone'_extensionProductIter _ h

Premises used: CategoryTheory.ObjectProperty.monotone'_extensionProductIter
-- 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 m : ℕ
h : n ≤ m
hP : P = ⊥
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

Tactic:
simp [hP]
-- 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 : ℕ
rw : P.triangEnvelopeIter 0 ≤ P.triangEnvelopeIter n
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ P.triangEnvelopeIter n

Tactic:
rw [← triangEnvelopeIter_zero]

Premises used: CategoryTheory.ObjectProperty.triangEnvelopeIter_zero
-- 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:
P.monotone'_triangEnvelopeIter (Nat.zero_le n)

Premises used: Nat.zero_le, CategoryTheory.ObjectProperty.monotone'_triangEnvelopeIter