awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ
⊢ (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)

Tactic:
simp [map, δ_zero_cochain_comp,
        Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p (by lia) (by lia)]

Premises used: add_neg_cancel, CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.mappingCone.map, HAdd.hAdd, OfNat.ofNat, CochainComplex.HomComplex.δ_zero_cochain_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₃
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
⊢ 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)

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₃
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:
simp [hom, inv, lift_desc_f _ _ _ _ _ _ _ n (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

Premises used: CochainComplex.MappingConeCompHomotopyEquiv.hom, CochainComplex.mappingCone.ext_from_iff, HAdd.hAdd, CochainComplex.mappingCone.lift_desc_f, OfNat.ofNat, rfl, CochainComplex.MappingConeCompHomotopyEquiv.inv
-- 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₃
⊢ HAdd.hAdd (α := ℤ) (-1) (-1) = -2

Tactic:
decide
-- 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₃
⊢ HAdd.hAdd (α := ℤ) 1 (-2) = -1

Tactic:
decide
-- 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₃
⊢ HAdd.hAdd (α := ℤ) (-1) 1 = 0

Tactic:
decide
-- 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₃
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
decide
-- 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₃
⊢ HAdd.hAdd (α := ℤ) (-2) 1 = -1

Tactic:
decide
-- 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₃
⊢ 2 = HAdd.hAdd (α := ℤ) 1 1

Tactic:
decide
-- 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 :
  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₁))
⊢ 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₁))

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]

Premises used: CochainComplex.mappingCone.δ_inl, CochainComplex.HomComplex.δ_neg, CochainComplex.HomComplex.Cochain.neg_comp, neg_neg, Int.negOnePow_neg, Int.negOnePow_one, CochainComplex.HomComplex.δ_comp, one_smul, CochainComplex.HomComplex.Cocycle.δ_eq_zero, CochainComplex.mappingCone.δ_snd, Units.neg_smul, neg_add_cancel, Exists.intro, Int.negOnePow_even, CochainComplex.HomComplex.Cochain.zero_comp, add_zero, OfNat.ofNat, CochainComplex.HomComplex.δ_zero_cochain_comp, Neg.neg
-- 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 :
  ∀ (n : ℤ),
    Cochain.v (Cochain.ofHom (inv f g ≫ hom f g)) n n ⋯ =
      (-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₁))).v
        n n ⋯
⊢ 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₁))

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₃
n : ℤ
⊢ n + 1 + 1 = n + 2

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₃
n : ℤ
⊢ n + 1 = n + 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₃
n : ℤ
⊢ n + 1 + -1 = n

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₃
n : ℤ
⊢ HAdd.hAdd (α := ℤ) 1 (-2) = -1

Tactic:
decide
-- 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₃
n : ℤ
⊢ n + 2 + -2 = n

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₃
n : ℤ
⊢ HAdd.hAdd (α := ℤ) (-1) (-1) = -2

Tactic:
decide
-- 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₃
n : ℤ
⊢ n + 2 + -1 = n + 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₃
n : ℤ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [ext_to_iff _ n (n + 1) rfl, map, Cochain.comp_v _ _
          (add_neg_cancel 1) n (n + 1) n (by lia) (by lia),
        Cochain.comp_v _ _ (show 1 + -2 = -1 by decide) (n + 1) (n + 2) n
          (by lia) (by lia),
        Cochain.comp_v _ _ (show (-1) + -1 = -2 by decide) (n + 2) (n + 1) n
          (by lia) (by lia)]

Premises used: add_neg_cancel, CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.mappingCone.map, 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₃
⊢ Eq (α := mappingCone g ⟶ mappingCone g)
    (CategoryStruct.comp (Y := mappingCone (mappingConeCompTriangle f g).mor₁) (MappingConeCompHomotopyEquiv.hom f g)
        (MappingConeCompHomotopyEquiv.inv f g) :
      mappingCone g ⟶ mappingCone g)
    (𝟙 (mappingCone g) : mappingCone g ⟶ mappingCone 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₃
⊢ Eq (α := mappingCone g ⟶ mappingCone g)
    (CategoryStruct.comp (Y := mappingCone (mappingConeCompTriangle f g).mor₁)
        (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g)) (HomotopyEquiv.inv (mappingConeCompHomotopyEquiv f g)) :
      mappingCone g ⟶ mappingCone g)
    (𝟙 (mappingCone g) : mappingCone g ⟶ mappingCone g)

Tactic:
simp [mappingConeCompHomotopyEquiv]

Premises used: CochainComplex.mappingConeCompHomotopyEquiv
-- 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₃
⊢ CategoryStruct.comp (Y :=
      mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
        (map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g)))
      (inr (map f (f ≫ g) (𝟙 X₁) g ⋯) :
        mappingCone (f ≫ g) ⟶
          mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
            (map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g)))
      (HomotopyEquiv.inv (mappingConeCompHomotopyEquiv f g) :
        mappingCone (mappingConeCompTriangle f g).mor₁ ⟶ mappingCone g) =
    (mappingConeCompTriangle f g).mor₂

Tactic:
simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.inv]

Premises used: CochainComplex.mappingConeCompHomotopyEquiv, CochainComplex.mappingCone.map, CochainComplex.MappingConeCompHomotopyEquiv.inv
-- 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 :
  ∀ (n : ℤ),
    (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n =
      (mappingConeCompTriangle f g).mor₃.f n
⊢ HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
    (mappingConeCompTriangle f g).mor₃

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₃
n : ℤ
⊢ (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g) ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n =
    (mappingConeCompTriangle f g).mor₃.f n

Tactic:
simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.hom,
    lift_f _ _ _ _ _ (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

Premises used: CochainComplex.mappingConeCompHomotopyEquiv, CochainComplex.MappingConeCompHomotopyEquiv.hom, CochainComplex.mappingCone.ext_from_iff, CochainComplex.mappingCone.map, HAdd.hAdd, OfNat.ofNat, CochainComplex.mappingCone.lift_f, 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₃
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)))
⊢ 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₁))

Tactic:
rw [← cancel_mono (HomotopyCategory.isoOfHomotopyEquiv
      (mappingConeCompHomotopyEquiv f g)).inv, assoc]

Premises used: CochainComplex.mappingConeCompHomotopyEquiv, CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, HomotopyCategory.isoOfHomotopyEquiv, CategoryTheory.Iso.inv
-- 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₃
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)

Tactic:
⟨_, _, (mappingConeCompTriangle f g).mor₁, ⟨?_⟩⟩

Premises used: Set.Mem, setOf, CochainComplex.mappingConeCompTriangle, Nonempty.intro, Exists.intro, CategoryTheory.Pretriangulated.Triangle.mor₁, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- 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₃
inst_3 : HasZeroObject.{v, u_1} C
refine : mappingConeCompTriangleh f g ≅ mappingCone.triangleh (mappingConeCompTriangle f g).mor₁
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) (mappingConeCompTriangleh f g)

Tactic:
refine ⟨_, _, (mappingConeCompTriangle f g).mor₁, ⟨?_⟩⟩
-- 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₃
inst_3 : HasZeroObject.{v, u_1} C
⊢ (mappingConeCompTriangleh f g).mor₂ ≫ Iso.hom (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)) =
    Iso.hom (Iso.refl (mappingConeCompTriangleh f g).obj₂) ≫
      (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₂

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₃
inst_3 : HasZeroObject.{v, u_1} C
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₃
⊢ mappingConeCompTriangleh f g ≅ mappingCone.triangleh (mappingConeCompTriangle f g).mor₁

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (isoOfHomotopyEquiv
    (mappingConeCompHomotopyEquiv f g)) (by cat_disch) (by simp) ?_

Premises used: CategoryTheory.Iso.refl, HomotopyCategory.isoOfHomotopyEquiv, CategoryTheory.Pretriangulated.Triangle.isoMk