awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
φ : T.obj₂ ⟶ T'.obj₂
a_1 b : ℤ
h₀ : t.IsLE T.obj₁ a_1
h₁' : t.IsGE T'.obj₃ b
h : a_1 < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
c : T.obj₃ ⟶ T'.obj₃
comm₂ : T.mor₂ ≫ c = φ ≫ T'.mor₂
comm₃ : T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T'.mor₃
⊢ ∃ (f : T ⟶ T'), f.hom₂ = φ

Tactic:
⟨{ hom₁ := a, hom₂ := φ, hom₃ := c }, rfl⟩

Premises used: Exists.intro, CategoryTheory.Pretriangulated.TriangleMorphism.mk, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
φ : T.obj₂ ⟶ T'.obj₂
a_1 b : ℤ
h₀ : t.IsLE T.obj₁ a_1
h₁' : t.IsGE T'.obj₃ b
h : a_1 < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
c : T.obj₃ ⟶ T'.obj₃
comm₂ : T.mor₂ ≫ c = φ ≫ T'.mor₂
comm₃ : T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T'.mor₃
⊢ ∃ (f : T ⟶ T'), f.hom₂ = φ

Tactic:
exact ⟨{ hom₁ := a, hom₂ := φ, hom₃ := c }, rfl⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
e : T.obj₂ ≅ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T.obj₃ b
h₀' : t.IsLE T'.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
obtain : ∀ (hom : T ⟶ T') (hhom : hom.hom₂ = e.hom), ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom
⊢ ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom

Tactic:
obtain ⟨hom, hhom⟩ := triangle_map_exists t hT hT' e.hom _ _ h₀ h₁'

Premises used: CategoryTheory.Triangulated.TStructure.triangle_map_exists, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
e : T.obj₂ ≅ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T.obj₃ b
h₀' : t.IsLE T'.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
hom : T ⟶ T'
hhom : hom.hom₂ = e.hom
obtain : ∀ (inv : T' ⟶ T), inv.hom₂ = e.inv → ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom
⊢ ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom

Tactic:
obtain ⟨inv, _⟩ := triangle_map_exists t hT' hT e.inv _ _ h₀' h₁

Premises used: CategoryTheory.Triangulated.TStructure.triangle_map_exists, CategoryTheory.inv, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
e : T.obj₂ ≅ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T.obj₃ b
h₀' : t.IsLE T'.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
hom : T ⟶ T'
hhom : hom.hom₂ = e.hom
inv : T' ⟶ T
h_1 : inv.hom₂ = e.inv
⊢ ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom

Tactic:
⟨{hom := hom
      inv := inv
      hom_inv_id := triangle_map_ext t hT hT a b h₀ h₁
      inv_hom_id := triangle_map_ext t hT' hT' a b h₀' h₁' }, hhom⟩

Premises used: CategoryTheory.Iso.mk, Exists.intro, CategoryTheory.Triangulated.TStructure.triangle_map_ext
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
e : T.obj₂ ≅ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T.obj₃ b
h₀' : t.IsLE T'.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
hom : T ⟶ T'
hhom : hom.hom₂ = e.hom
inv : T' ⟶ T
h_1 : inv.hom₂ = e.inv
⊢ ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom

Tactic:
exact
    ⟨{hom := hom
      inv := inv
      hom_inv_id := triangle_map_ext t hT hT a b h₀ h₁
      inv_hom_id := triangle_map_ext t hT' hT' a b h₀' h₁' }, hhom⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X : C
⊢ n - 1 + 1 = n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n_1 : ℤ
X : C
n : ℤ
⊢ n - 1 + 1 = n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
f₁ f₂ : triangle t n X ⟶ triangle t n Y
H : f₁.hom₂ = f₂.hom₂
⊢ n - 1 ≤ n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
⊢ n - 1 < n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
H : ∃ (f : triangle t n X ⟶ triangle t n Y), f.hom₂ = φ
rw :
  (triangle t n X).mor₁ ≫ φ =
    (triangle t n X).mor₁ ≫ H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₂
rw₁ rw₂ : (triangle t n X).mor₁ ≫ φ = (triangle t n X).mor₁ ≫ φ
⊢ (triangle t n X).mor₁ ≫ φ =
    H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₁ ≫ (triangle t n Y).mor₁

Tactic:
rw [← H.choose.comm₁, H.choose_spec]

Premises used: Exists.choose_spec, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, Exists.choose
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
H : ∃ (f : triangle t n X ⟶ triangle t n Y), f.hom₂ = φ
rw :
  H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₂ ≫ (triangle t n Y).mor₂ =
    φ ≫ (triangle t n Y).mor₂
rw₁ rw₂ : φ ≫ (triangle t n Y).mor₂ = φ ≫ (triangle t n Y).mor₂
⊢ (triangle t n X).mor₂ ≫ H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₃ =
    φ ≫ (triangle t n Y).mor₂

Tactic:
rw [H.choose.comm₂, H.choose_spec]

Premises used: Exists.choose_spec, Exists.choose, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
A : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((triangleFunctor t n).obj A)

Tactic:
triangle_distinguished t n A

Premises used: Set.Mem, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_distinguished, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle, CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
dsimp : t.IsLE (triangle t n A).obj₁ (n - 1)
⊢ t.IsLE ((triangleFunctor t n).obj A).obj₁ (n - 1)

Tactic:
dsimp [triangleFunctor]

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
⊢ t.IsLE (triangle t n A).obj₁ (n - 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
dsimp : t.IsGE (triangle t n A).obj₃ n
⊢ t.IsGE ((triangleFunctor t n).obj A).obj₃ n

Tactic:
dsimp [triangleFunctor]

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
⊢ t.IsGE (triangle t n A).obj₃ n

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ (f : triangle t a A ⟶ triangle t b A), f.hom₂ = 𝟙 (triangle t a A).obj₂
rw :
  (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ =
    (triangle t a A).mor₁ ≫
      H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₂
rw₁ rw₂ : (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ = (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂
⊢ (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ =
    H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₁ ≫
      (triangle t b A).mor₁

Tactic:
rw [← H.choose.comm₁, H.choose_spec]

Premises used: Exists.choose_spec, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, Exists.choose
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ (f : triangle t a A ⟶ triangle t b A), f.hom₂ = 𝟙 (triangle t a A).obj₂
rw :
  H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₂ ≫
      (triangle t b A).mor₂ =
    𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
rw₁ rw₂ : 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂ = 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
⊢ (triangle t a A).mor₂ ≫
      H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₃ =
    𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂

Tactic:
rw [H.choose.comm₂, H.choose_spec]

Premises used: Exists.choose_spec, Exists.choose, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : ?m.28
a b : ℤ
h : a ≤ b
x x_1 : C
x_2 : x ⟶ x_1
⊢ ((triangleFunctor t a).map x_2 ≫ triangleMapOfLE t x_1 a b h).hom₂ =
    (triangleMapOfLE t x a b h ≫ (triangleFunctor t b).map x_2).hom₂

Tactic:
simp [triangleMapOfLE]

Premises used: _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b : ℤ
h : a ≤ b
X : C
⊢ ((triangleFunctorNatTransOfLE t a b h).app X).hom₂ = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
app :
  (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app =
    (triangleFunctorNatTransOfLE t a c ⋯).app
⊢ triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc = triangleFunctorNatTransOfLE t a c ⋯

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
app :
  ∀ (X : C),
    (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app X =
      (triangleFunctorNatTransOfLE t a c ⋯).app X
⊢ (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app =
    (triangleFunctorNatTransOfLE t a c ⋯).app

Tactic:
ext1 X
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app X).hom₂ =
    ((triangleFunctorNatTransOfLE t a c ⋯).app X).hom₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app X =
    (triangleFunctorNatTransOfLE t a c ⋯).app X

Tactic:
exact triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _)
    (triangleFunctor_obj_distinguished _ _ _) (a - 1) c inferInstance inferInstance (by simp)

Premises used: HSub.hSub, inferInstance, CategoryTheory.Triangulated.TStructure.triangle_map_ext, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_obj_distinguished, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
X Y : C
φ : X ⟶ Y
A : ?m.28
a : ℤ
⊢ a ≤ a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
app : (triangleFunctorNatTransOfLE t a a ⋯).app = NatTrans.app (𝟙 (triangleFunctor t a))
⊢ triangleFunctorNatTransOfLE t a a ⋯ = 𝟙 (triangleFunctor t a)

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
app : ∀ (X : C), (triangleFunctorNatTransOfLE t a a ⋯).app X = NatTrans.app (𝟙 (triangleFunctor t a)) X
⊢ (triangleFunctorNatTransOfLE t a a ⋯).app = NatTrans.app (𝟙 (triangleFunctor t a))

Tactic:
ext1 X
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
X : C
⊢ ((triangleFunctorNatTransOfLE t a a ⋯).app X).hom₂ = (NatTrans.app (𝟙 (triangleFunctor t a)) X).hom₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
a : ℤ
X : C
⊢ (triangleFunctorNatTransOfLE t a a ⋯).app X = NatTrans.app (𝟙 (triangleFunctor t a)) X

Tactic:
exact triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _)
    (triangleFunctor_obj_distinguished _ _ _) (a - 1) a inferInstance inferInstance (by simp)

Premises used: HSub.hSub, inferInstance, CategoryTheory.Triangulated.TStructure.triangle_map_ext, _private.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_obj_distinguished, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
x x_1 : C
x_2 x_3 : x ⟶ x_1
dsimp :
  Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))
⊢ (t.truncLT n).map (x_2 + x_3) = (t.truncLT n).map x_2 + (t.truncLT n).map x_3

Tactic:
dsimp only [truncLT, Functor.comp_map]

Premises used: CategoryTheory.Triangulated.TStructure.truncLT, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
n : ℤ
x x_1 : C
x_2 x_3 : x ⟶ x_1
rw :
  Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2 + (TruncAux.triangleFunctor t n).map x_3) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))
⊢ Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))

Tactic:
rw [Functor.map_add]

Premises used: CategoryTheory.Functor.map_add