awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
⊢ (f ≫ g) ≫ 𝟙 X₃ = f ≫ g
have rw : f ≫ g = f ≫ g
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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'
⊢ 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'))
have 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) sorry ≫ (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) sorry))
        n :
      (mappingCone g).X n ⟶
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (mappingConeCompTriangle f' g').obj₁).X
          n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 ⟶
      (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)
have 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') sorry) 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') sorry)
        (n + 1)) :
    (mappingCone g).X n ⟶ (mappingCone f').X (n + 1))
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
⊢ 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
have h : ∀ (p : ℤ),
  (HAdd.hAdd (α := Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₂ 1)
          (δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) sorry))
          (Cochain.comp
            (↑(descCocycle g (Cochain.ofHom (inr f)) 0 sorry sorry :
                  Cocycle (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1) :
              Cochain (mappingCone g) (mappingConeCompTriangle f g).obj₁ 1)
            (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) sorry)).v
      p (p + 1) sorry =
    Cochain.v 0 p (p + 1) sorry
Tactic: ext p _ rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 (α := 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) ⋯
have 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))) sorry)) p (p + 1) sorry :
      (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1))
    (Cochain.v
        (Cochain.comp (G := mappingCone f) (descCochain g (Cochain.ofHom (inr f)) 0 sorry)
          (Cochain.ofHom
            (desc f ((Cochain.ofHom (𝟙 X₁)).comp (inl (f ≫ g)) mapOfHomotopy._proof_2) (g ≫ inr (f ≫ g)) sorry))
          sorry)
        p (p + 1) sorry :
      (mappingCone g).X p ⟶ (mappingCone (f ≫ g)).X (p + 1)) =
  0
Tactic: dsimp [mappingConeCompTriangle, map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 (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)
have h : ∀ (p : ℤ),
  Eq (α := (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
    (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) sorry)) p p sorry :
      (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) sorry) (inr g) sorry))
        p p sorry :
      (mappingConeCompTriangle f g).obj₁.X p ⟶ (mappingCone g).X p)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 : ℤ
⊢ 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)
have h : (CategoryStruct.comp (Y := (mappingCone g).X p)
        (CategoryStruct.comp (Y := (mappingCone f).X p) (Cochain.v (inl f) (p + 1) p sorry)
          (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) sorry)) p p sorry))
        (Cochain.v (↑(fst g) : Cochain (mappingCone g) X₂ 1) p (p + 1) sorry) =
      CategoryStruct.comp (Y := (mappingCone g).X p)
        (Cochain.v (inl f) (p + 1) p sorry ≫
            Cochain.v
              (Cochain.ofHom
                ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) sorry) (inr g) sorry))
              p p sorry :
          X₁.X (p + 1) ⟶ (mappingCone g).X p)
        (Cochain.v (↑(fst g) : Cochain (mappingCone g) X₂ 1) p (p + 1) sorry : (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 sorry)
          (Cochain.v (δ (-1) 0 (Cochain.comp (snd f) (inl g) sorry)) p p sorry))
        (Cochain.v (snd g) p p sorry) =
      CategoryStruct.comp (Y := (mappingCone g).X p)
        (Cochain.v (inl f) (p + 1) p sorry ≫
            Cochain.v
              (Cochain.ofHom
                ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) sorry) (inr g) sorry))
              p p sorry :
          X₁.X (p + 1) ⟶ (mappingCone g).X p)
        (Cochain.v (snd g) p p sorry : (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) sorry)) p p sorry) :
      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) sorry) (inr g) sorry))
          p p sorry :
      X₂.X p ⟶ (mappingCone g).X p)
Tactic: rw [ext_from_iff _ (p + 1) _ rfl, ext_to_iff _ _ (p + 1) rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 (α := mappingCone g ⟶ mappingCone g)
    (CategoryStruct.comp (Y := mappingCone (mappingConeCompTriangle f g).mor₁) (hom f g) (inv f g) :
      mappingCone g ⟶ mappingCone g)
    (𝟙 (mappingCone g) : mappingCone g ⟶ mappingCone g)
have h : ∀ (n : ℤ),
  HomologicalComplex.Hom.f
      (CategoryStruct.comp (Y := mappingCone (mappingConeCompTriangle f g).mor₁) (hom f g) (inv f g)) n =
    HomologicalComplex.Hom.f (𝟙 (mappingCone g)) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    δ (-1) 0
        (-Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
            (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
              (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
have rw : Cochain.ofHom (inv f g ≫ hom f g) =
  -HAdd.hAdd (α :=
        Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingCone (mappingConeCompTriangle f g).mor₁) 0)
        (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
          (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
            (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
              (Cochain.comp (inl f)
                (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) sorry)
              (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) sorry))
            sorry)
          sorry)
        (Cochain.comp
          (Cochain.comp
            (↑(fst (mappingConeCompTriangle f g).mor₁) :
              Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁ 1)
            (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) sorry)
          (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
            (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) sorry)
          sorry) +
    Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
Tactic: rw [δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
        Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul,
        δ_comp _ _ (show 1 + (-2) = -1 by decide) 2 (-1) 0 (by decide)
          (by decide) (by decide),
        δ_comp _ _ (show (-1) + (-1) = -2 by decide) 0 0 (-1) (by decide)
          (by decide) (by decide), Int.negOnePow_neg, Int.negOnePow_neg,
        Int.negOnePow_even 2 ⟨1, by decide⟩, Int.negOnePow_one, Units.neg_smul,
        one_smul, one_smul, δ_inl, δ_inl, δ_snd, Cocycle.δ_eq_zero, Cochain.zero_comp, add_zero,
        Cochain.neg_comp, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -HAdd.hAdd (α :=
          Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingCone (mappingConeCompTriangle f g).mor₁) 0)
          (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
            (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
              (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                (Cochain.comp (inl f)
                  (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯)
                (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) ⋯))
              ⋯)
            ⋯)
          (Cochain.comp
            (Cochain.comp
              (↑(fst (mappingConeCompTriangle f g).mor₁) :
                Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁ 1)
              (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯)
            (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
              (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
have h : ∀ (n : ℤ),
  Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n sorry =
    (-HAdd.hAdd (α :=
              Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingCone (mappingConeCompTriangle f g).mor₁)
                0)
              (Cochain.comp (snd (mappingConeCompTriangle f g).mor₁)
                (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                  (HAdd.hAdd (α := Cochain X₁ (mappingCone (mappingConeCompTriangle f g).mor₁) (-1))
                    (Cochain.comp (inl f)
                      (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) sorry)
                    (-Cochain.comp (Cochain.ofHom (f ≫ inr f)) (inl (mappingConeCompTriangle f g).mor₁) sorry))
                  sorry)
                sorry)
              (Cochain.comp
                (Cochain.comp
                  (↑(fst (mappingConeCompTriangle f g).mor₁) :
                    Cochain (mappingCone (mappingConeCompTriangle f g).mor₁) (mappingConeCompTriangle f g).obj₁ 1)
                  (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) sorry)
                (Cochain.comp (↑(fst (f ≫ g)) : Cochain (mappingCone (f ≫ g)) X₁ 1)
                  (Cochain.comp (inl f) (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) sorry)
                sorry) +
          Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))).v
      n n sorry
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
⊢ HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
    (mappingConeCompTriangle f g).mor₃
have h : ∀ (n : ℤ),
  (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n =
    (mappingConeCompTriangle f g).mor₃.f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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 (α :=
    (mappingConeCompTriangleh f g).obj₂ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (mappingConeCompTriangle f g).mor₁))
    ((mappingConeCompTriangleh f g).mor₂ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g)))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (inr (mappingConeCompTriangle f g).mor₁))
have rw : (mappingConeCompTriangleh f g).mor₂ ≫
    CategoryStruct.comp (Y :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (mappingConeCompTriangle f g).mor₁))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g)))
      (Iso.inv (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g))) =
  CategoryStruct.comp (Y :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (mappingConeCompTriangle f g).mor₁))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (inr (mappingConeCompTriangle f g).mor₁))
    (Iso.inv (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)))
Tactic: rw [← cancel_mono (HomotopyCategory.isoOfHomotopyEquiv
      (mappingConeCompHomotopyEquiv f g)).inv, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) (mappingConeCompTriangleh f g)
have refine : mappingConeCompTriangleh f g ≅ mappingCone.triangleh (mappingConeCompTriangle f g).mor₁
Tactic: refine ⟨_, _, (mappingConeCompTriangle f g).mor₁, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ mappingConeCompTriangleh f g ≅ mappingCone.triangleh (mappingConeCompTriangle f g).mor₁
have refine : (mappingConeCompTriangleh f g).mor₃ ≫
    CategoryTheory.Functor.map
      (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Iso.hom (Iso.refl (mappingConeCompTriangleh f g).obj₁)) =
  Iso.hom (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)) ≫
    (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₃
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (isoOfHomotopyEquiv
    (mappingConeCompHomotopyEquiv f g)) (by cat_disch) (by simp) ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Triangulated (goal)
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₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f)))
    (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (mappingCone f)))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        ((mappingCone.triangle g).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
            (mappingCone.inr f)))
      (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f)))
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
        (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
          (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f))
have e_a : (mappingCone.triangle g).mor₃ ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
      (mappingCone.inr f) =
  HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫
    (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
        (mappingCone.map f (f ≫ g) (𝟙 X₁) g sorry : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : HasZeroObject.{v, u} V
⊢ IsZero (C := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0)
have rw : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
  (𝟙 (Functor.obj (quotient V c) 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]