awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
w w_1 w_2 : CochainComplex.{v_1, u_1, 0} C ℤ
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (Pretriangulated.Triangle.mk (X :=
      Functor.obj (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (Functor.obj (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 ⋯ ⋯)
          (ComposableArrows.mk₂ f g)))
      (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (NatTrans.app
          (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 0 2 2 SpectralObject._proof_6
            SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4)
          (ComposableArrows.mk₂ f g)))
      (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (NatTrans.app
          (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 2 1 2 2 SpectralObject._proof_8
            SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4)
          (ComposableArrows.mk₂ f g)))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 2) ↦
            Pretriangulated.Triangle.mor₃
              (Functor.obj (Functor.mapTriangle (quotient C (ComplexShape.up ℤ)))
                (CochainComplex.mappingConeCompTriangle
                  (D.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
                  (D.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))),
          naturality := ⋯ }
        (ComposableArrows.mk₂ f g)))

Tactic:
HomotopyCategory.mappingConeCompTriangleh_distinguished f g

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, Set.Mem, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.Mk₁.map, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.Pretriangulated.Triangle.mk, CochainComplex.mappingConeCompTriangleh, HomotopyCategory.mappingConeCompTriangleh_distinguished
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
w w_1 w_2 : CochainComplex.{v_1, u_1, 0} C ℤ
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Membership.mem (γ := Set (Pretriangulated.Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@CategoryTheory.Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (Pretriangulated.Triangle.mk (X :=
      Functor.obj (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (Functor.obj (ComposableArrows.functorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 2 ⋯ ⋯)
          (ComposableArrows.mk₂ f g)))
      (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (NatTrans.app
          (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 1 0 2 2 SpectralObject._proof_6
            SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4)
          (ComposableArrows.mk₂ f g)))
      (CategoryTheory.Functor.map (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ))
        (NatTrans.app
          (ComposableArrows.mapFunctorArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 0 2 1 2 2 SpectralObject._proof_8
            SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4)
          (ComposableArrows.mk₂ f g)))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows (CochainComplex.{v_1, u_1, 0} C ℤ) 2) ↦
            Pretriangulated.Triangle.mor₃
              (Functor.obj (Functor.mapTriangle (quotient C (ComplexShape.up ℤ)))
                (CochainComplex.mappingConeCompTriangle
                  (D.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
                  (D.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))),
          naturality := ⋯ }
        (ComposableArrows.mk₂ f g)))

Tactic:
exact HomotopyCategory.mappingConeCompTriangleh_distinguished f g

Premises used: HomotopyCategory.mappingConeCompTriangleh_distinguished
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
rw rw₁ : f ≫ g = f ≫ g
⊢ f ≫ g = 𝟙 X₁ ≫ f ≫ g

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
rw rw₁ : f ≫ g = f ≫ g
⊢ (f ≫ g) ≫ 𝟙 X₃ = f ≫ g

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex.{v, u_1, 0} C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
h :
  ∀ (n : ℤ),
    Eq (α :=
      (mappingCone g).X n ⟶
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (mappingConeCompTriangle f' g').obj₁).X
          n)
      (HomologicalComplex.Hom.f (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (mappingConeCompTriangle f' g').mor₃) n :
        (mappingCone g).X n ⟶
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
                (mappingConeCompTriangle f' g').obj₁).X
            n)
      (HomologicalComplex.Hom.f
          ((mappingConeCompTriangle f g).mor₃ ≫
            CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (map f f' (φ.app 0) (φ.app 1) ⋯))
          n :
        (mappingCone g).X n ⟶
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
                (mappingConeCompTriangle f' g').obj₁).X
            n)
⊢ Eq (α :=
    mappingCone g ⟶
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
        (mappingConeCompTriangle f' g').obj₁)
    (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (mappingConeCompTriangle f' g').mor₃ :
      mappingCone g ⟶
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
          (mappingConeCompTriangle f' g').obj₁)
    ((mappingConeCompTriangle f g).mor₃ ≫
        CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
          (map f f' (φ.app 0) (φ.app 1) ⋯) :
      (mappingConeCompTriangle f g).obj₃ ⟶
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1) (mappingCone f'))

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex.{v, u_1, 0} C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
h :
  Eq (α := (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))
    (CategoryStruct.comp (Y := (mappingCone g').X n)
        (HomologicalComplex.Hom.f
            (desc g (Cochain.comp (Cochain.ofHom (φ.app 1)) (inl g') mapOfHomotopy._proof_2) (φ.app 2 ≫ inr g') ⋯) n :
          (mappingCone g).X n ⟶ (mappingCone g').X n)
        ((triangle g').mor₃.f n ≫ HomologicalComplex.Hom.f (inr f') (n + 1) :
          (mappingCone g').X n ⟶ (mappingCone f').X (n + 1)) :
      (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))
    (CategoryStruct.comp (Y := (mappingCone f).X (n + 1))
        ((triangle g).mor₃.f n ≫ HomologicalComplex.Hom.f (inr f) (n + 1))
        (HomologicalComplex.Hom.f
          (desc f (Cochain.comp (Cochain.ofHom (φ.app 0)) (inl f') mapOfHomotopy._proof_2) (φ.app 1 ≫ inr f') ⋯)
          (n + 1)) :
      (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))
⊢ Eq (α :=
    (mappingCone g).X n ⟶
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
            (mappingConeCompTriangle f' g').obj₁).X
        n)
    (HomologicalComplex.Hom.f (map g g' (φ.app 1) (φ.app 2) ⋯ ≫ (mappingConeCompTriangle f' g').mor₃) n :
      (mappingCone g).X n ⟶
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (mappingConeCompTriangle f' g').obj₁).X
          n)
    (HomologicalComplex.Hom.f
        ((mappingConeCompTriangle f g).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
            (map f f' (φ.app 0) (φ.app 1) ⋯))
        n :
      (mappingCone g).X n ⟶
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (mappingConeCompTriangle f' g').obj₁).X
          n)

Tactic:
dsimp [map]

Premises used: CochainComplex.mappingCone.map
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
Y₁ Y₂ Y₃ : CochainComplex.{v, u_1, 0} C ℤ
f' : Y₁ ⟶ Y₂
g' : Y₂ ⟶ Y₃
φ : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ Eq (α := (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))
    (CategoryStruct.comp (Y := (mappingCone g').X n)
        (HomologicalComplex.Hom.f
            (desc g (Cochain.comp (Cochain.ofHom (φ.app 1)) (inl g') mapOfHomotopy._proof_2) (φ.app 2 ≫ inr g') ⋯) n :
          (mappingCone g).X n ⟶ (mappingCone g').X n)
        ((triangle g').mor₃.f n ≫ HomologicalComplex.Hom.f (inr f') (n + 1) :
          (mappingCone g').X n ⟶ (mappingCone f').X (n + 1)) :
      (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))
    (CategoryStruct.comp (Y := (mappingCone f).X (n + 1))
        ((triangle g).mor₃.f n ≫ HomologicalComplex.Hom.f (inr f) (n + 1))
        (HomologicalComplex.Hom.f
          (desc f (Cochain.comp (Cochain.ofHom (φ.app 0)) (inl f') mapOfHomotopy._proof_2) (φ.app 1 ≫ inr f') ⋯)
          (n + 1)) :
      (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))

Tactic:
simp only [Int.reduceNeg, Fin.isValue, assoc, inr_f_desc_f, HomologicalComplex.comp_f,
    ext_from_iff _ (n + 1) _ rfl, inl_v_desc_f_assoc, Cochain.zero_cochain_comp_v, Cochain.ofHom_v,
    inl_v_triangle_mor₃_f_assoc, triangle_obj₁, shiftFunctor_obj_X', shiftFunctor_obj_X,
    shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, Preadditive.neg_comp,
    id_comp, Preadditive.comp_neg, inr_f_desc_f_assoc, inr_f_triangle_mor₃_f_assoc, zero_comp,
    comp_zero, and_self]

Premises used: CategoryTheory.Category.assoc, and_self, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingCone.ext_from_iff, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.mappingCone.inr_f_desc_f, CochainComplex.mappingCone.inl_v_desc_f_assoc, CochainComplex.shiftFunctorObjXIso, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, HomologicalComplex.comp_f, CategoryTheory.Iso.refl_inv, Fin.isValue, HAdd.hAdd, CochainComplex.shiftFunctor_obj_X', CategoryTheory.Preadditive.neg_comp, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CategoryTheory.Limits.zero_comp, OfNat.ofNat, rfl, CochainComplex.mappingCone.triangle_obj₁, CochainComplex.mappingCone.inr_f_desc_f_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ δ 0 1 (Cochain.ofHom (inr f)) =
    HSMul.hSMul (β := Cochain X₂ (mappingConeCompTriangle f g).obj₁ 1) (Int.negOnePow 1)
      ((Cochain.ofHom g).comp (↑0 : Cochain X₃ (mappingConeCompTriangle f g).obj₁ 1) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
h :
  ∀ (p : ℤ),
    (HAdd.hAdd (α := Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₂ 1)
            (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯))
            (Cochain.comp
              (↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯ :
                    Cocycle (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1) :
                Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1)
              (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)).v
        p (p + 1) ⋯ =
      Cochain.v 0 p (p + 1) ⋯
⊢ HAdd.hAdd (α := Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₂ 1)
      (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯))
      (Cochain.comp
        (↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯ : Cocycle (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1) :
          Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1)
        (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯) =
    0

Tactic:
ext p _ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
h :
  HAdd.hAdd (α := (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1)) (β :=
      (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1))
      (Cochain.v (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯)) p (p + 1) ⋯ :
        (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1))
      (Cochain.v
          (Cochain.comp (G := mappingCone f) (descCochain g (Cochain.ofHom (inr f)) 0 ⋯)
            (Cochain.ofHom
              (desc f ((Cochain.ofHom (𝟙 X₁)).comp (inl (f ≫ g)) mapOfHomotopy._proof_2) (g ≫ inr (f ≫ g)) ⋯))
            ⋯)
          p (p + 1) ⋯ :
        (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1)) =
    0
⊢ (HAdd.hAdd (α := Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₂ 1)
          (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯))
          (Cochain.comp
            (↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯ :
                  Cocycle (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1) :
              Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1)
            (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)).v
      p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯

Tactic:
dsimp [mappingConeCompTriangle, map]

Premises used: CochainComplex.mappingCone.map, CochainComplex.mappingConeCompTriangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ p + 1 + -1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ p + 2 + -1 = p + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ HAdd.hAdd (α := (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1)) (β :=
      (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1))
      (Cochain.v (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯)) p (p + 1) ⋯ :
        (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1))
      (Cochain.v
          (Cochain.comp (G := mappingCone f) (descCochain g (Cochain.ofHom (inr f)) 0 ⋯)
            (Cochain.ofHom
              (desc f ((Cochain.ofHom (𝟙 X₁)).comp (inl (f ≫ g)) mapOfHomotopy._proof_2) (g ≫ inr (f ≫ g)) ⋯))
            ⋯)
          p (p + 1) ⋯ :
        (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1)) =
    0

Tactic:
simp [ext_from_iff _ _ _ rfl, inl_v_d_assoc _ (p + 1) p (p + 2) (by lia) (by lia)]

Premises used: CochainComplex.mappingCone.ext_from_iff, CochainComplex.mappingCone.inl_v_d_assoc, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Eq (α := Cochain X₁ (mappingCone g) 0) (δ (-1) 0 ((Cochain.ofHom f).comp (inl g) ⋯)) (Cochain.ofHom ((f ≫ g) ≫ inr g))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
h :
  ∀ (p : ℤ),
    Eq (α := (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
      (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) ⋯)) p p ⋯ :
        (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
      (Cochain.v
          (Cochain.ofHom
            ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯))
          p p ⋯ :
        (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
⊢ Eq (α := Cochain (mappingConeCompTriangle f g).obj₁ (mappingCone g) 0)
    (δ (-1) 0 (Cochain.comp (snd f) (inl g) ⋯) : Cochain (mappingConeCompTriangle f g).obj₁ (mappingCone g) 0)
    (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯) :
      Cochain (mappingConeCompTriangle f g).obj₁ (mappingCone g) 0)

Tactic:
ext p
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
h :
  (CategoryStruct.comp (Y := (mappingCone g).X p)
          (CategoryStruct.comp (Y := (mappingCone f).X p) (Cochain.v (inl f) (p + 1) p ⋯)
            (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) ⋯)) p p ⋯))
          (Cochain.v (↑(fst g) : Cochain (mappingCone g) X₂ 1) p (p + 1) ⋯) =
        CategoryStruct.comp (Y := (mappingCone g).X p)
          (Cochain.v (inl f) (p + 1) p ⋯ ≫
              Cochain.v
                (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯))
                p p ⋯ :
            X₁.X (p + 1) ⟶ (mappingCone g).X p)
          (Cochain.v (↑(fst g) : Cochain (mappingCone g) X₂ 1) p (p + 1) ⋯ : (mappingCone g).X p ⟶ X₂.X (p + 1)) ∧
      CategoryStruct.comp (Y := (mappingCone g).X p)
          (CategoryStruct.comp (Y := (mappingCone f).X p) (Cochain.v (inl f) (p + 1) p ⋯)
            (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) ⋯)) p p ⋯))
          (Cochain.v (snd g) p p ⋯) =
        CategoryStruct.comp (Y := (mappingCone g).X p)
          (Cochain.v (inl f) (p + 1) p ⋯ ≫
              Cochain.v
                (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯))
                p p ⋯ :
            X₁.X (p + 1) ⟶ (mappingCone g).X p)
          (Cochain.v (snd g) p p ⋯ : (mappingCone g).X p ⟶ X₃.X p)) ∧
    Eq (α := X₂.X p ⟶ (mappingCone g).X p)
      (CategoryStruct.comp (Y := (mappingCone f).X p) (HomologicalComplex.Hom.f (inr f) p)
          (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) ⋯)) p p ⋯) :
        X₂.X p ⟶ (mappingCone g).X p)
      (HomologicalComplex.Hom.f (inr f) p ≫
          Cochain.v
            (Cochain.ofHom
              ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯))
            p p ⋯ :
        X₂.X p ⟶ (mappingCone g).X p)
⊢ Eq (α := (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
    (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) ⋯)) p p ⋯ :
      (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
    (Cochain.v
        (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯))
        p p ⋯ :
      (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)

Tactic:
rw [ext_from_iff _ (p + 1) _ rfl, ext_to_iff _ _ (p + 1) rfl]

Premises used: CochainComplex.mappingCone.ext_from_iff, CochainComplex.mappingCone.ext_to_iff, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ p + 1 = p + 1

Tactic:
lia