awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
dsimp :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂))
    ((CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₁) ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a))
    (CategoryStruct.comp (Y := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₂).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₂ :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂)))
⊢ (triangleh φ₁).mor₃ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a) =
    CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ (triangleh φ₂).mor₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₂))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₁ ≫
        CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
⊢ Eq (α := Cochain K₁ (mappingCone φ₂) 0) (δ (-1) 0 ((Cochain.ofHom a).comp (inl φ₂) ⋯))
    (Cochain.ofHom (φ₁ ≫ b ≫ inr φ₂))

Tactic:
simp [reassoc_of% comm]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
⊢ Eq (α := mappingCone φ₁ ⟶ mappingCone φ₂) (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂)
    (mapOfHomotopy (Homotopy.ofEq comm) : mappingCone φ₁ ⟶ mappingCone φ₂)

Tactic:
simp [map, mapOfHomotopy]

Premises used: CochainComplex.mappingCone.map, CochainComplex.mappingCone.mapOfHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
rw : φ ≫ 𝟙 L = φ
rw₁ rw₂ : φ = φ
⊢ φ ≫ 𝟙 L = 𝟙 K ≫ φ

Tactic:
rw [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
h : ∀ (n : ℤ), HomologicalComplex.Hom.f (map φ φ (𝟙 K) (𝟙 L) ⋯) n = HomologicalComplex.Hom.f (𝟙 (mappingCone φ)) n
⊢ Eq (α := mappingCone φ ⟶ mappingCone φ) (map φ φ (𝟙 K) (𝟙 L) ⋯ : mappingCone φ ⟶ mappingCone φ)
    (𝟙 (mappingCone φ) : mappingCone φ ⟶ mappingCone φ)

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ HomologicalComplex.Hom.f (map φ φ (𝟙 K) (𝟙 L) ⋯) n = HomologicalComplex.Hom.f (𝟙 (mappingCone φ)) n

Tactic:
simp [ext_from_iff _ (n + 1) n rfl, map]

Premises used: CochainComplex.mappingCone.ext_from_iff, CochainComplex.mappingCone.map, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
rw : a ≫ φ₂ ≫ b' = (a ≫ a') ≫ φ₃
rw₁ : a ≫ a' ≫ φ₃ = (a ≫ a') ≫ φ₃
rw₂ rw₃ : a ≫ a' ≫ φ₃ = a ≫ a' ≫ φ₃
⊢ φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃

Tactic:
rw [reassoc_of% comm, comm', assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
h :
  ∀ (n : ℤ),
    Eq (α := (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
      (HomologicalComplex.Hom.f (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯) n : (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
      (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y := mappingCone φ₂) (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂)
            (map φ₂ φ₃ a' b' comm' : mappingCone φ₂ ⟶ mappingCone φ₃))
          n :
        (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
⊢ Eq (α := mappingCone φ₁ ⟶ mappingCone φ₃) (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯ : mappingCone φ₁ ⟶ mappingCone φ₃)
    (CategoryStruct.comp (Y := mappingCone φ₂) (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂)
        (map φ₂ φ₃ a' b' comm' : mappingCone φ₂ ⟶ mappingCone φ₃) :
      mappingCone φ₁ ⟶ mappingCone φ₃)

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
n : ℤ
⊢ Eq (α := (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
    (HomologicalComplex.Hom.f (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯) n : (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
    (HomologicalComplex.Hom.f
        (CategoryStruct.comp (Y := mappingCone φ₂) (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂)
          (map φ₂ φ₃ a' b' comm' : mappingCone φ₂ ⟶ mappingCone φ₃))
        n :
      (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)

Tactic:
simp [ext_from_iff _ (n + 1) n rfl, map]

Premises used: CochainComplex.mappingCone.ext_from_iff, CochainComplex.mappingCone.map, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
dsimp :
  Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
⊢ (triangle φ₁).mor₂ ≫ map φ₁ φ₂ a b comm = b ≫ (triangle φ₂).mor₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
rw :
  Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (mapOfHomotopy (Homotopy.ofEq comm) : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
rw₁ rw₂ : Eq (α := L₁ ⟶ mappingCone φ₂) (b ≫ inr φ₂) (b ≫ inr φ₂)
⊢ Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)

Tactic:
rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₂]

Premises used: CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, CochainComplex.mappingCone.map_eq_mapOfHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
dsimp :
  (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃
⊢ (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
rw :
  (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    mapOfHomotopy (Homotopy.ofEq comm) ≫ (triangle φ₂).mor₃
rw₁ rw₂ :
  (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a
⊢ (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃

Tactic:
rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₃]

Premises used: CochainComplex.mappingCone.map_eq_mapOfHomotopy, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ HAdd.hAdd (α :=
      Cochain
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          K)
        (mappingCone φ) 1)
      (δ 0 1 (-Cochain.leftShift (inl φ) 1 0 ⋯))
      (Cochain.comp
        (↑(-(Cocycle.ofHom φ).leftShift 1 1 ⋯) :
          Cochain ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj K) L 1)
        (Cochain.ofHom (inr φ)) ⋯) =
    0

Tactic:
simp only [Int.reduceNeg, δ_neg,
        Cochain.δ_leftShift _ 1 0 1 (neg_add_cancel 1) 0 (zero_add 1),
        Int.negOnePow_one, δ_inl, Cochain.ofHom_comp, Cochain.leftShift_comp_zero_cochain,
        Units.neg_smul, one_smul, neg_neg, Cocycle.coe_neg, Cocycle.leftShift_coe,
        Cocycle.ofHom_coe, Cochain.neg_comp, add_neg_cancel]

Premises used: CochainComplex.mappingCone.δ_inl, add_neg_cancel, CochainComplex.HomComplex.δ_neg, Int.reduceNeg, CochainComplex.HomComplex.Cochain.neg_comp, CochainComplex.HomComplex.Cocycle.coe_neg, neg_neg, Int.negOnePow_one, zero_add, one_smul, Units.neg_smul, neg_add_cancel, CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain, CochainComplex.HomComplex.Cocycle.ofHom_coe, OfNat.ofNat, CochainComplex.HomComplex.Cocycle.leftShift_coe, CochainComplex.HomComplex.Cochain.δ_leftShift, CochainComplex.HomComplex.Cochain.ofHom_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ δ (-1) 0 0 = Cochain.ofHom (inr φ ≫ (triangle φ).mor₃)

Tactic:
simp only [δ_zero, inr_triangleδ, Cochain.ofHom_zero]

Premises used: CochainComplex.mappingCone.inr_triangleδ, CochainComplex.HomComplex.δ_zero, CochainComplex.HomComplex.Cochain.ofHom_zero
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
h :
  ∀ (n : ℤ),
    (CategoryStruct.comp (Y := mappingCone (G := mappingCone φ) (inr φ))
            (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯ :
              Functor.obj
                  (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K ⟶
                mappingCone (G := mappingCone φ) (inr φ))
            (desc (inr φ) 0 (triangle φ).mor₃ ⋯ :
              mappingCone (G := mappingCone φ) (inr φ) ⟶
                Functor.obj
                  (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
                  K)).f
        n =
      HomologicalComplex.Hom.f
        (𝟙
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            K))
        n
⊢ CategoryStruct.comp (Y := mappingCone (G := mappingCone φ) (inr φ))
      (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯ :
        Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            K ⟶
          mappingCone (G := mappingCone φ) (inr φ))
      (desc (inr φ) 0 (triangle φ).mor₃ ⋯ :
        mappingCone (G := mappingCone φ) (inr φ) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            K) =
    𝟙 (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K)

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
simp only [add_neg_cancel_right]

Premises used: add_neg_cancel_right
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ (CategoryStruct.comp (Y := mappingCone (G := mappingCone φ) (inr φ))
          (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯ :
            Functor.obj
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K ⟶
              mappingCone (G := mappingCone φ) (inr φ))
          (desc (inr φ) 0 (triangle φ).mor₃ ⋯ :
            mappingCone (G := mappingCone φ) (inr φ) ⟶
              Functor.obj
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K)).f
      n =
    HomologicalComplex.Hom.f
      (𝟙
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          K))
      n

Tactic:
simp only [shiftFunctor_obj_X', Int.reduceNeg, HomologicalComplex.comp_f,
      lift_desc_f _ _ _ _ _ _ _ _ _ rfl, Cocycle.coe_neg, Cocycle.leftShift_coe,
      Cocycle.ofHom_coe, Cochain.neg_v, Cochain.zero_v,
      comp_zero, (inl φ).leftShift_v 1 0 _ _ n _ (n + 1) (by simp only [add_neg_cancel_right]),
      shiftFunctor_obj_X, mul_zero, sub_self, Int.zero_ediv, add_zero, Int.negOnePow_zero,
      shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, id_comp, one_smul,
      Preadditive.neg_comp, inl_v_triangle_mor₃_f, Iso.refl_inv, neg_neg, zero_add,
      HomologicalComplex.id_f]

Premises used: sub_self, CochainComplex.HomComplex.Cochain.neg_v, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CategoryTheory.Limits.comp_zero, CochainComplex.HomComplex.Cochain.zero_v, HomologicalComplex.id_f, CochainComplex.shiftFunctor_obj_X, CochainComplex.HomComplex.Cocycle.coe_neg, neg_neg, CochainComplex.shiftFunctorObjXIso, HomologicalComplex.comp_f, zero_add, one_smul, MulZeroClass.mul_zero, CategoryTheory.Iso.refl_inv, HAdd.hAdd, Int.zero_ediv, Int.negOnePow_zero, CochainComplex.mappingCone.lift_desc_f, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.shiftFunctor_obj_X', CategoryTheory.Preadditive.neg_comp, CochainComplex.HomComplex.Cocycle.ofHom_coe, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cocycle.leftShift_coe, CategoryTheory.Iso.refl_hom, rfl, CochainComplex.mappingCone.inl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
h :
  ∀ (n : ℤ),
    Cochain.v
        (Cochain.ofHom
          (desc (inr φ) 0 (triangle φ).mor₃ ⋯ ≫
            lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯))
        n n ⋯ =
      (δ (-1) 0 (-Cochain.comp (snd (inr φ)) (Cochain.comp (snd φ) (inl (inr φ)) ⋯) ⋯) +
            Cochain.ofHom (𝟙 (mappingCone (G := mappingCone φ) (inr φ)))).v
        n n ⋯
⊢ Cochain.ofHom
      (desc (inr φ) 0 (triangle φ).mor₃ ⋯ ≫
        lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯) =
    δ (-1) 0 (-Cochain.comp (snd (inr φ)) (Cochain.comp (snd φ) (inl (inr φ)) ⋯) ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (G := mappingCone φ) (inr φ)))

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
⊢ n + 1 + 0 = n + 1

Tactic:
lia