mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₂ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₃ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((rotate C ⋙ rotate C ⋙ rotate C).obj T).mor₁ ≫ (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₂).hom =
    (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₁).hom ≫ ((Triangle.shiftFunctor C 1).obj T).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((rotate C ⋙ rotate C ⋙ rotate C).obj T).mor₂ ≫ (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₃).hom =
    (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₂).hom ≫ ((Triangle.shiftFunctor C 1).obj T).mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((rotate C ⋙ rotate C ⋙ rotate C).obj T).mor₃ ≫
      (shiftFunctor C 1).map (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₁).hom =
    (Iso.refl ((rotate C ⋙ rotate C ⋙ rotate C).obj T).obj₃).hom ≫ ((Triangle.shiftFunctor C 1).obj T).mor₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).mor₁ ≫
      (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₂).hom =
    (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₁).hom ≫ ((Triangle.shiftFunctor C (-1)).obj T).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).mor₂ ≫
      (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₃).hom =
    (Iso.refl ((invRotate C ⋙ invRotate C ⋙ invRotate C).obj T).obj₂).hom ≫ ((Triangle.shiftFunctor C (-1)).obj T).mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₁ ≫
      (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₁) =
    (eqToHom ⋯).hom₁ ≫
      (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₁)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₂ ≫
      (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₂) =
    (eqToHom ⋯).hom₂ ≫
      (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₂)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₃ ≫
      (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₃) =
    (eqToHom ⋯).hom₃ ≫
      (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₃)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom =
    (shiftFunctor C (-1)).mapZeroObject.symm.hom ≫ (contractibleTriangle X).invRotate.mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₂ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom ≫ (contractibleTriangle X).invRotate.mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₃ ≫ (shiftFunctor C 1).map (shiftFunctor C (-1)).mapZeroObject.symm.hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom ≫ (contractibleTriangle X).invRotate.mor₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₁ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom =
    ((shiftEquiv C 1).unitIso.app X).hom ≫ (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate.mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).mor₂ ≫
      (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₃).hom =
    (Iso.refl (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X))).obj₂).hom ≫
      (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate.mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0

pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0

pp: case refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0

pp: case refine_4
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ (shiftFunctor C 1).map (𝟙 X) = 0 ≫ 0

Tactic:
all_goals apply Subsingleton.elim

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
h : IsZero T.obj₃
x✝ : IsIso T.mor₁
⊢ T.mor₁ ≫ (asIso T.mor₁).symm.hom = (Iso.refl T.obj₁).hom ≫ (contractibleTriangle T.obj₁).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
h : IsZero T.obj₁
⊢ IsIso T.rotate.mor₁ ↔ IsIso T.mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
h : IsZero T.obj₂
⊢ IsIso T.rotate.mor₂ ↔ IsIso T.mor₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
⊢ f ≫ φ.hom₂ = 0 → f = 0

Tactic:
hf

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
⊢ f = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ g ≫ T.mor₁ ≫ φ.hom₂ = 0

Tactic:
hf

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
⊢ (y₂ ≫ T'.mor₂ ≫ inv φ.hom₃) ≫ φ.hom₃ = y₂ ≫ T'.mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
⊢ (y₁ ≫ inv φ.hom₁) ≫ φ.hom₁ = y₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
x₁ : A ⟶ T.obj₁
hx₁ : x₁ ≫ φ.hom₁ = y₁
⊢ (x₂ + x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂

Tactic:
rw [add_comp, assoc, φ.comm₁, reassoc_of% hx₁, ← hy₁, add_sub_cancel]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
⊢ BinaryBiproductData T.obj₁ T.obj₃

Tactic:
have : Mono T.mor₁ := T.mono₁ hT hT₀

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
⊢ BinaryBiproductData T.obj₁ T.obj₃
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X₁ X₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem : Triangle.mk inl snd 0 ∈ distinguishedTriangles
⊢ 𝟙 X₃ ≫ (Triangle.mk inl snd 0).mor₃ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
⊢ (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) ≫ T.mor₂ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ section_ T.mor₂ ≫ T.mor₂ = 𝟙 T.obj₃

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ (inr φ ≫ (triangle φ).mor₃).f i✝ = HomologicalComplex.Hom.f 0 i✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (inl (𝟙 K)).comp (Cochain.ofHom (𝟙 (mappingCone (𝟙 K)))) ⋯ =
    δ (-2) (-1) 0 + (Cochain.ofHom (𝟙 K)).comp (inl (𝟙 K)) ⋯ + (inl (𝟙 K)).comp (Cochain.ofHom 0) ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ Cochain.ofHom (inr (𝟙 K) ≫ 𝟙 (mappingCone (𝟙 K))) = δ (-1) 0 (inl (𝟙 K)) + Cochain.ofHom (inr (𝟙 K) ≫ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ δ (-1) 0
      ((Cochain.ofHom a).comp (inl φ₂) ⋯ +
        (↑((Cochain.equivHomotopy (φ₁ ≫ b) (a ≫ φ₂)) H)).comp (Cochain.ofHom (inr φ₂)) ⋯) =
    Cochain.ofHom (φ₁ ≫ b ≫ inr φ₂)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem : Triangle.mk g h 0 ∈ distinguishedTriangles
e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ (Triangle.mk g h 0).mor₃ ≫ (shiftFunctor C 1).map (Iso.refl (Triangle.mk g h 0).obj₁).hom =
    (Iso.refl (Triangle.mk g h 0).obj₃).hom ≫ (binaryBiproductTriangle X₁ X₂).mor₃

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫
      (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₁ ≫
        (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a) ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (triangleh φ).rotate.mor₁ ≫ (Iso.refl (triangleh φ).rotate.obj₂).hom =
    (Iso.refl (triangleh φ).rotate.obj₁).hom ≫ (triangleh (inr φ)).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (triangleh φ).rotate.mor₂ ≫
      ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).symm.app K ≪≫
          HomotopyCategory.isoOfHomotopyEquiv (rotateHomotopyEquiv φ)).hom =
    (Iso.refl (triangleh φ).rotate.obj₂).hom ≫ (triangleh (inr φ)).mor₂

Tactic:
simp

Goal state after: