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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
X₁ X₂ : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X₁ X₂
⊢ (binaryProductTriangle X₁ X₂).mor₂ ≫ (Iso.refl (binaryProductTriangle X₁ X₂).obj₃).hom =
    (biprod.isoProd X₁ X₂).symm.hom ≫ (binaryBiproductTriangle X₁ X₂).mor₂

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
X₁ X₂ : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X₁ X₂
⊢ (binaryProductTriangle X₁ X₂).mor₃ ≫ (shiftFunctor C 1).map (Iso.refl (binaryProductTriangle X₁ X₂).obj₁).hom =
    (Iso.refl (binaryProductTriangle X₁ X₂).obj₃).hom ≫ (binaryBiproductTriangle X₁ X₂).mor₃

Tactic:
by 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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₁).hom ≫ ((𝟭 (Triangle C)).obj T).mor₁

Tactic:
by 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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₂).hom ≫ ((𝟭 (Triangle C)).obj T).mor₂

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ 𝟙 ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) = 0

Tactic:
rw [← Functor.map_id, h₁, Functor.map_zero]

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:
by 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✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Epi f
⊢ IsSplitEpi f

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
    obtain ⟨r, hr⟩ := Triangle.coyoneda_exact₂ _ hT (𝟙 _)
      (by rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, comp_zero])
    exact ⟨r, hr.symm⟩

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₂
⊢ (y₂ ≫ T'.mor₂ ≫ inv φ.hom₃) ≫ φ.hom₃ = y₂ ≫ T'.mor₂

Tactic:
by 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₂ ≫ T'.mor₂ - x₃ ≫ φ.hom₃ = 0

Tactic:
hx₃,

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₃
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₂ ≫ T'.mor₂ - y₂ ≫ T'.mor₂ = 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₂
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:
by 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:
add_comp,

Goal state after:
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₂ ≫ φ.hom₂ + (x₁ ≫ T.mor₁) ≫ φ.hom₂ = y₂
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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
⊢ contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)

Tactic:
have h := (isZero_quotient_obj_iff _).2 ⟨CochainComplex.mappingCone.homotopyToZeroOfId X⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ contractibleTriangle { as := X } ≅ CochainComplex.mappingCone.triangleh (𝟙 X)
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
inst✝ : HasZeroObject C
X : HomologicalComplex C (ComplexShape.up ℤ)
h : IsZero ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (𝟙 X)))
⊢ (contractibleTriangle { as := X }).mor₁ ≫ (Iso.refl (contractibleTriangle { as := X }).obj₂).hom =
    (Iso.refl (contractibleTriangle { as := X }).obj₁).hom ≫ (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₁

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
n : ℤ
T : Triangle C
⊢ ((Triangle.shiftFunctor C n ⋙ F.mapTriangle).obj T).mor₁ ≫ ((commShiftIso F n).app T.obj₂).hom =
    ((commShiftIso F n).app T.obj₁).hom ≫ ((F.mapTriangle ⋙ Triangle.shiftFunctor D n).obj T).mor₁

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
n : ℤ
T : Triangle C
⊢ ((Triangle.shiftFunctor C n ⋙ F.mapTriangle).obj T).mor₂ ≫ ((commShiftIso F n).app T.obj₃).hom =
    ((commShiftIso F n).app T.obj₂).hom ≫ ((F.mapTriangle ⋙ Triangle.shiftFunctor D n).obj T).mor₂

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
T : Triangle C
⊢ ((F.mapTriangle ⋙ rotate D).obj T).mor₁ ≫ (Iso.refl ((F.mapTriangle ⋙ rotate D).obj T).obj₂).hom =
    (Iso.refl ((F.mapTriangle ⋙ rotate D).obj T).obj₁).hom ≫ ((rotate C ⋙ F.mapTriangle).obj T).mor₁

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
T : Triangle C
⊢ ((F.mapTriangle ⋙ rotate D).obj T).mor₂ ≫ ((commShiftIso F 1).symm.app T.obj₁).hom =
    (Iso.refl ((F.mapTriangle ⋙ rotate D).obj T).obj₂).hom ≫ ((rotate C ⋙ F.mapTriangle).obj T).mor₂

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
T : Triangle C
⊢ ((F.mapTriangle ⋙ rotate D).obj T).mor₃ ≫
      (shiftFunctor D 1).map (Iso.refl ((F.mapTriangle ⋙ rotate D).obj T).obj₁).hom =
    ((commShiftIso F 1).symm.app T.obj₁).hom ≫ ((rotate C ⋙ F.mapTriangle).obj T).mor₃

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ ((σ p).s ≫ S.X₂.d p (p + 1) ≫ (σ (p + 1)).r ≫ S.X₁.d (p + 1) (p + 2) +
        S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r) ≫
      S.f.f (p + 2) =
    0 ≫ S.f.f (p + 2)

Tactic:
add_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ ((σ p).s ≫ S.X₂.d p (p + 1) ≫ (σ (p + 1)).r ≫ S.X₁.d (p + 1) (p + 2)) ≫ S.f.f (p + 2) +
      (S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r) ≫ S.f.f (p + 2) =
    0 ≫ S.f.f (p + 2)
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
T : Triangle C
⊢ ((F.mapTriangle ⋙ invRotate D).obj T).mor₁ ≫ (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj T).obj₂).hom =
    ((commShiftIso F (-1)).symm.app T.obj₃).hom ≫ ((invRotate C ⋙ F.mapTriangle).obj T).mor₁

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
T : Triangle C
⊢ ((F.mapTriangle ⋙ invRotate D).obj T).mor₂ ≫ (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj T).obj₃).hom =
    (Iso.refl ((F.mapTriangle ⋙ invRotate D).obj T).obj₂).hom ≫ ((invRotate C ⋙ F.mapTriangle).obj T).mor₂

Tactic:
by simp

Goal state after: