awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A : Triangle.{v, u} C
⊢ TriangleMorphism.hom₂ (𝟙 A) = 𝟙 A.obj₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A : Triangle.{v, u} C
⊢ TriangleMorphism.hom₃ (𝟙 A) = 𝟙 A.obj₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
X Y Z : Triangle.{v, u} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom₁ = f.hom₁ ≫ g.hom₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
X Y Z : Triangle.{v, u} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom₂ = f.hom₂ ≫ g.hom₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
X Y Z : Triangle.{v, u} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom₃ = f.hom₃ ≫ g.hom₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁
comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂
comm₃ : A.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) iso₁.hom = iso₃.hom ≫ B.mor₃
⊢ B.mor₁ ≫ iso₂.inv = iso₁.inv ≫ A.mor₁

Tactic:
simp only [← cancel_mono iso₂.hom, assoc, Iso.inv_hom_id, comp_id,
      comm₁, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁
comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂
comm₃ : A.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) iso₁.hom = iso₃.hom ≫ B.mor₃
⊢ B.mor₂ ≫ iso₃.inv = iso₂.inv ≫ A.mor₂

Tactic:
simp only [← cancel_mono iso₃.hom, assoc, Iso.inv_hom_id, comp_id,
      comm₂, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁
comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂
comm₃ : A.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) iso₁.hom = iso₃.hom ≫ B.mor₃
⊢ B.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) iso₁.inv = iso₃.inv ≫ A.mor₃

Tactic:
simp only [← cancel_mono (iso₁.hom⟦(1 : ℤ)⟧'), Category.assoc, comm₃,
      Iso.inv_hom_id_assoc, ← Functor.map_comp, Iso.inv_hom_id,
      Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.shiftFunctor, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₁ ≫ (asIso f.hom₂).hom = (asIso f.hom₁).hom ≫ B.mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₂ ≫ (asIso f.hom₃).hom = (asIso f.hom₂).hom ≫ B.mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (asIso f.hom₁).hom = (asIso f.hom₃).hom ≫ B.mor₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
e : A ≅ B := A.isoMk B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃) ⋯ ⋯ ⋯
⊢ IsIso f

Tactic:
(inferInstance : IsIso e.hom)

Premises used: inferInstance, CategoryTheory.Pretriangulated.Triangle.homMk
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
e : A ≅ B := A.isoMk B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃) ⋯ ⋯ ⋯
⊢ IsIso f

Tactic:
exact (inferInstance : IsIso e.hom)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₁ = 𝟙 A.obj₁
rw₁ : TriangleMorphism.hom₁ (𝟙 A) = 𝟙 A.obj₁
rw₂ rw₃ : Eq.{v + 1} (α := A.obj₁ ⟶ A.obj₁) (𝟙 A.obj₁) (𝟙 A.obj₁)
⊢ e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 A.obj₁

Tactic:
rw [← comp_hom₁, e.hom_inv_id, id_hom₁]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Pretriangulated.comp_hom₁, CategoryTheory.Pretriangulated.id_hom₁
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₂ = 𝟙 A.obj₂
rw₁ : TriangleMorphism.hom₂ (𝟙 A) = 𝟙 A.obj₂
rw₂ rw₃ : Eq.{v + 1} (α := A.obj₂ ⟶ A.obj₂) (𝟙 A.obj₂) (𝟙 A.obj₂)
⊢ e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂

Tactic:
rw [← comp_hom₂, e.hom_inv_id, id_hom₂]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Pretriangulated.id_hom₂, CategoryTheory.Pretriangulated.comp_hom₂
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₃ = 𝟙 A.obj₃
rw₁ : TriangleMorphism.hom₃ (𝟙 A) = 𝟙 A.obj₃
rw₂ rw₃ : Eq.{v + 1} (α := A.obj₃ ⟶ A.obj₃) (𝟙 A.obj₃) (𝟙 A.obj₃)
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃

Tactic:
rw [← comp_hom₃, e.hom_inv_id, id_hom₃]

Premises used: CategoryTheory.Pretriangulated.id_hom₃, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Pretriangulated.comp_hom₃
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₁ = 𝟙 B.obj₁
rw₁ : TriangleMorphism.hom₁ (𝟙 B) = 𝟙 B.obj₁
rw₂ rw₃ : Eq.{v + 1} (α := B.obj₁ ⟶ B.obj₁) (𝟙 B.obj₁) (𝟙 B.obj₁)
⊢ e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁

Tactic:
rw [← comp_hom₁, e.inv_hom_id, id_hom₁]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Pretriangulated.comp_hom₁, CategoryTheory.Pretriangulated.id_hom₁
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₂ = 𝟙 B.obj₂
rw₁ : TriangleMorphism.hom₂ (𝟙 B) = 𝟙 B.obj₂
rw₂ rw₃ : Eq.{v + 1} (α := B.obj₂ ⟶ B.obj₂) (𝟙 B.obj₂) (𝟙 B.obj₂)
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂

Tactic:
rw [← comp_hom₂, e.inv_hom_id, id_hom₂]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Pretriangulated.id_hom₂, CategoryTheory.Pretriangulated.comp_hom₂
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₃ = 𝟙 B.obj₃
rw₁ : TriangleMorphism.hom₃ (𝟙 B) = 𝟙 B.obj₃
rw₂ rw₃ : Eq.{v + 1} (α := B.obj₃ ⟶ B.obj₃) (𝟙 B.obj₃) (𝟙 B.obj₃)
⊢ e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃

Tactic:
rw [← comp_hom₃, e.inv_hom_id, id_hom₃]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Pretriangulated.id_hom₃, CategoryTheory.Pretriangulated.comp_hom₃
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
h : A = B
subst : A.obj₁ = A.obj₁
⊢ A.obj₁ = B.obj₁

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A : Triangle.{v, u} C
⊢ A.obj₁ = A.obj₁

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
h : A = B
subst : TriangleMorphism.hom₁ (eqToHom ⋯) = eqToHom ⋯
⊢ TriangleMorphism.hom₁ (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A : Triangle.{v, u} C
⊢ TriangleMorphism.hom₁ (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
h : A = B
subst : A.obj₂ = A.obj₂
⊢ A.obj₂ = B.obj₂

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A : Triangle.{v, u} C
⊢ A.obj₂ = A.obj₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
h : A = B
subst : TriangleMorphism.hom₂ (eqToHom ⋯) = eqToHom ⋯
⊢ TriangleMorphism.hom₂ (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A : Triangle.{v, u} C
⊢ TriangleMorphism.hom₂ (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
h : A = B
subst : A.obj₃ = A.obj₃
⊢ A.obj₃ = B.obj₃

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A : Triangle.{v, u} C
⊢ A.obj₃ = A.obj₃

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
h : A = B
subst : TriangleMorphism.hom₃ (eqToHom ⋯) = eqToHom ⋯
⊢ TriangleMorphism.hom₃ (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A : Triangle.{v, u} C
⊢ TriangleMorphism.hom₃ (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
h₁ : (f + g + h).hom₁ = (f + (g + h)).hom₁
h₂ : (f + g + h).hom₂ = (f + (g + h)).hom₂
h₃ : (f + g + h).hom₃ = (f + (g + h)).hom₃
⊢ f + g + h = f + (g + h)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
⊢ (f + g + h).hom₁ = (f + (g + h)).hom₁

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
⊢ (f + g + h).hom₂ = (f + (g + h)).hom₂

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
⊢ (f + g + h).hom₃ = (f + (g + h)).hom₃

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (0 + f).hom₁ = f.hom₁
h₂ : (0 + f).hom₂ = f.hom₂
h₃ : (0 + f).hom₃ = f.hom₃
⊢ 0 + f = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (0 + f).hom₁ = f.hom₁

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (0 + f).hom₂ = f.hom₂

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (0 + f).hom₃ = f.hom₃

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (f + 0).hom₁ = f.hom₁
h₂ : (f + 0).hom₂ = f.hom₂
h₃ : (f + 0).hom₃ = f.hom₃
⊢ f + 0 = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (f + 0).hom₁ = f.hom₁

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (f + 0).hom₂ = f.hom₂

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (f + 0).hom₃ = f.hom₃

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : ((n + 1) • f).hom₁ = (n • f + f).hom₁
h₂ : ((n + 1) • f).hom₂ = (n • f + f).hom₂
h₃ : ((n + 1) • f).hom₃ = (n • f + f).hom₃
⊢ (n + 1) • f = n • f + f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ ((n + 1) • f).hom₁ = (n • f + f).hom₁

Tactic:
apply AddMonoid.nsmul_succ

Premises used: AddMonoid.nsmul_succ
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ ((n + 1) • f).hom₂ = (n • f + f).hom₂

Tactic:
apply AddMonoid.nsmul_succ

Premises used: AddMonoid.nsmul_succ
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ ((n + 1) • f).hom₃ = (n • f + f).hom₃

Tactic:
apply AddMonoid.nsmul_succ

Premises used: AddMonoid.nsmul_succ
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
h₁ : (f - g).hom₁ = (f + -g).hom₁
h₂ : (f - g).hom₂ = (f + -g).hom₂
h₃ : (f - g).hom₃ = (f + -g).hom₃
⊢ f - g = f + -g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ (f - g).hom₁ = (f + -g).hom₁

Tactic:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ (f - g).hom₂ = (f + -g).hom₂

Tactic:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ (f - g).hom₃ = (f + -g).hom₃

Tactic:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₁
h₂ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₂
h₃ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₃ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₃
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f = HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₁

Tactic:
apply SubNegMonoid.zsmul_succ'

Premises used: SubNegMonoid.zsmul_succ'
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₂

Tactic:
apply SubNegMonoid.zsmul_succ'

Premises used: SubNegMonoid.zsmul_succ'
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₃ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₃

Tactic:
apply SubNegMonoid.zsmul_succ'

Premises used: SubNegMonoid.zsmul_succ'
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : (Int.negSucc n • f).hom₁ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁
h₂ : (Int.negSucc n • f).hom₂ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂
h₃ : (Int.negSucc n • f).hom₃ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₃
⊢ Int.negSucc n • f = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (Int.negSucc n • f).hom₁ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁

Tactic:
apply SubNegMonoid.zsmul_neg'

Premises used: SubNegMonoid.zsmul_neg'
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (Int.negSucc n • f).hom₂ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂

Tactic:
apply SubNegMonoid.zsmul_neg'

Premises used: SubNegMonoid.zsmul_neg'
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (Int.negSucc n • f).hom₃ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₃

Tactic:
apply SubNegMonoid.zsmul_neg'

Premises used: SubNegMonoid.zsmul_neg'
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (-f + f).hom₁ = TriangleMorphism.hom₁ 0
h₂ : (-f + f).hom₂ = TriangleMorphism.hom₂ 0
h₃ : (-f + f).hom₃ = TriangleMorphism.hom₃ 0
⊢ -f + f = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (-f + f).hom₁ = TriangleMorphism.hom₁ 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (-f + f).hom₂ = TriangleMorphism.hom₂ 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ (-f + f).hom₃ = TriangleMorphism.hom₃ 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
h₁ : (f + g).hom₁ = (g + f).hom₁
h₂ : (f + g).hom₂ = (g + f).hom₂
h₃ : (f + g).hom₃ = (g + f).hom₃
⊢ f + g = g + f

Tactic:
ext