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
n p : ℤ
refine_2 :
  Eq (α :=
    L.X (p + n) ⟶
      (mappingCone (F := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
            (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).X
        p)
    (HSMul.hSMul (β := L.X (p + n) ⟶ (mappingCone φ).X (p + n)) n.negOnePow (HomologicalComplex.Hom.f (inr φ) (p + n)) ≫
        HomologicalComplex.Hom.f (Iso.hom (shiftIso φ n)) p :
      L.X (p + n) ⟶
        (mappingCone (F := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).X
          p)
    (HSMul.hSMul (β := L.X (p + n) ⟶ L.X (p + n)) n.negOnePow (𝟙 (L.X (p + n))) ≫
        HomologicalComplex.Hom.f
          (inr (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)) p :
      L.X (p + n) ⟶
        (mappingCone (F := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).X
          p)
⊢ HomologicalComplex.Hom.f
      ((Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₂ ≫
        Iso.hom (shiftIso φ n))
      p =
    ((HSMul.hSMul (β :=
              (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₂ ≅
                (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₂)
              n.negOnePow
              (Iso.refl
                (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₂)).hom ≫
          (triangle (K := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).mor₂).f
      p

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
n p : ℤ
⊢ Eq (α :=
    L.X (p + n) ⟶
      (mappingCone (F := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
            (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).X
        p)
    (HSMul.hSMul (β := L.X (p + n) ⟶ (mappingCone φ).X (p + n)) n.negOnePow (HomologicalComplex.Hom.f (inr φ) (p + n)) ≫
        HomologicalComplex.Hom.f (Iso.hom (shiftIso φ n)) p :
      L.X (p + n) ⟶
        (mappingCone (F := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).X
          p)
    (HSMul.hSMul (β := L.X (p + n) ⟶ L.X (p + n)) n.negOnePow (𝟙 (L.X (p + n))) ≫
        HomologicalComplex.Hom.f
          (inr (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)) p :
      L.X (p + n) ⟶
        (mappingCone (F := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).X
          p)

Tactic:
simp only [Units.smul_def, shiftIso, Int.reduceNeg, Linear.smul_comp, id_comp,
      ext_to_iff _ _ (p + 1) rfl, shiftFunctor_obj_X', assoc, lift_f_fst_v, Cocycle.coe_smul,
      Cocycle.shift_coe, Cochain.smul_v, Cochain.shift_v', Linear.comp_smul, inr_f_fst_v,
      smul_zero, lift_f_snd_v, inr_f_snd_v, and_true]

Premises used: CategoryTheory.Category.assoc, CochainComplex.HomComplex.Cocycle.coe_smul, CochainComplex.mappingCone.shiftIso, CochainComplex.mappingCone.inr_f_fst_v, and_true, CochainComplex.mappingCone.lift_f_fst_v, Int.reduceNeg, smul_zero, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.mappingCone.ext_to_iff, CategoryTheory.Linear.comp_smul, HAdd.hAdd, CochainComplex.HomComplex.Cochain.smul_v, Units.smul_def, CochainComplex.HomComplex.Cocycle.shift_coe, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.lift_f_snd_v, OfNat.ofNat, CochainComplex.HomComplex.Cochain.shift_v', rfl, CategoryTheory.Linear.smul_comp, 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
n : ℤ
refine_3 :
  ∀ (p : ℤ),
    ((Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₃ ≫
            CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
              (Iso.hom
                (Iso.refl
                  (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₁))).f
        p =
      HomologicalComplex.Hom.f
        (Iso.hom (shiftIso φ n) ≫
          (triangle (K := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).mor₃)
        p
⊢ (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom
          (Iso.refl (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₁)) =
    Iso.hom (shiftIso φ n) ≫
      (triangle (K := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).mor₃

Tactic:
ext p
-- 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 p : ℤ
refine_3 :
  (n.negOnePow •
        (triangle φ).mor₃.f (p + n) ≫
          HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) 1 n)) K)
            p) ≫
      𝟙 (K.X (p + 1 + n)) =
    HomologicalComplex.Hom.f (Iso.hom (shiftIso φ n)) p ≫
      (triangle (K := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).mor₃.f
        p
⊢ ((Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
            (Iso.hom
              (Iso.refl
                (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₁))).f
      p =
    HomologicalComplex.Hom.f
      (Iso.hom (shiftIso φ n) ≫
        (triangle (K := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
            (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).mor₃)
      p

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
n p : ℤ
⊢ p + n + 1 = p + 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 p : ℤ
⊢ (n.negOnePow •
        (triangle φ).mor₃.f (p + n) ≫
          HomologicalComplex.Hom.f (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) 1 n)) K)
            p) ≫
      𝟙 (K.X (p + 1 + n)) =
    HomologicalComplex.Hom.f (Iso.hom (shiftIso φ n)) p ≫
      (triangle (K := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)).mor₃.f
        p

Tactic:
simp only [triangle, Triangle.mk_mor₃, Cocycle.homOf_f, Cocycle.rightShift_coe,
      Cocycle.coe_neg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
      (fst φ).1.rightShift_v 1 0 (zero_add 1) (p + n) (p + n) (add_zero (p + n)) (p + 1 + n)
        (by lia),
      shiftFunctor_obj_X, shiftFunctorObjXIso, shiftFunctorComm_hom_app_f, Preadditive.neg_comp,
      assoc, Iso.inv_hom_id, comp_id, smul_neg, Units.smul_def, shiftIso, Int.reduceNeg,
      (fst (φ⟦n⟧')).1.rightShift_v 1 0 (zero_add 1) p p (add_zero p) (p + 1) rfl,
      HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, Preadditive.comp_neg, lift_f_fst_v,
      Cocycle.coe_smul, Cocycle.shift_coe, Cochain.smul_v, Cochain.shift_v']

Premises used: CategoryTheory.Category.assoc, CochainComplex.HomComplex.Cocycle.coe_smul, CochainComplex.mappingCone.shiftIso, CategoryTheory.Iso.inv_hom_id, CochainComplex.HomComplex.Cochain.neg_v, CochainComplex.mappingCone.lift_f_fst_v, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CategoryTheory.shiftFunctor, CochainComplex.shiftFunctor_obj_X, CochainComplex.HomComplex.Cocycle.coe_neg, smul_neg, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, zero_add, CategoryTheory.Functor.map, CochainComplex.HomComplex.Cocycle.homOf_f, CategoryTheory.Iso.refl_inv, HAdd.hAdd, CochainComplex.HomComplex.Cochain.smul_v, Units.smul_def, CochainComplex.mappingCone.fst, CochainComplex.HomComplex.Cocycle.shift_coe, CochainComplex.shiftFunctor_obj_X', CategoryTheory.Preadditive.neg_comp, CochainComplex.shiftFunctorComm_hom_app_f, CochainComplex.HomComplex.Cochain.rightShift_neg, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Subtype.val, CochainComplex.HomComplex.Cochain.shift_v', CategoryTheory.Pretriangulated.Triangle.mk_mor₃, CochainComplex.mappingCone.triangle, rfl, CochainComplex.HomComplex.Cocycle.rightShift_coe
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
h :
  G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    HAdd.hAdd (α :=
        G.obj ((mappingCone φ).X n) ⟶
          HomologicalComplex.X
            (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯) ≫
          Cochain.v (inl (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n ⋯)
        (G.map (Cochain.v (snd φ) n n ⋯) ≫
          HomologicalComplex.Hom.f (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n) ≫
      HomologicalComplex.Hom.f
        (Triangle.mor₃
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
        n
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    CategoryStruct.comp (Y :=
      HomologicalComplex.X
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
      (Iso.hom (mapHomologicalComplexXIso φ G n) :
        G.obj ((mappingCone φ).X n) ⟶
          HomologicalComplex.X
            (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
      (HomologicalComplex.Hom.f
          (Triangle.mor₃
            (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
          n :
        HomologicalComplex.X
            (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n ⟶
          HomologicalComplex.X
            (Functor.obj
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)) (A := ℤ) 1)
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K))
            n)

Tactic:
rw [mapHomologicalComplexXIso_eq φ G n (n + 1) rfl, mapHomologicalComplexXIso'_hom]

Premises used: CochainComplex.mappingCone.mapHomologicalComplexXIso_eq, HAdd.hAdd, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
h : G.map ((triangle φ).mor₃.f n) = -G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯)
⊢ G.map ((triangle φ).mor₃.f n) ≫ 𝟙 (G.obj (K.X (n + 1))) =
    HAdd.hAdd (α :=
        G.obj ((mappingCone φ).X n) ⟶
          HomologicalComplex.X
            (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
              (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n)
        (G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯) ≫
          Cochain.v (inl (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n ⋯)
        (G.map (Cochain.v (snd φ) n n ⋯) ≫
          HomologicalComplex.Hom.f (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
            n) ≫
      HomologicalComplex.Hom.f
        (Triangle.mor₃
          (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
            (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
        n

Tactic:
simp only [Functor.mapHomologicalComplex_obj_X, add_comp, assoc, inl_v_triangle_mor₃_f,
    shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv,
    comp_neg, comp_id, inr_f_triangle_mor₃_f, comp_zero, add_zero]

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex.XIsoOfEq_rfl, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctor_obj_X, CategoryTheory.Functor.mapHomologicalComplex_obj_X, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CategoryTheory.Preadditive.add_comp, CategoryTheory.Iso.refl_inv, add_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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
h :
  Eq (α := G.obj ((mappingCone φ).X n) ⟶ G.obj (K.X (n + 1)))
    (G.map (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) n n ⋯))
    (-G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯))
⊢ G.map ((triangle φ).mor₃.f n) = -G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯)

Tactic:
dsimp [triangle]

Premises used: CochainComplex.mappingCone.triangle
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ HAdd.hAdd (α := ℤ) 0 1 = 1

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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ n + 0 = 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ n + 1 = n + 1

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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
h :
  Eq (α := G.obj ((mappingCone φ).X n) ⟶ G.obj (K.X (n + 1)))
    (G.map
      (Cochain.v (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) n (n + 1) ⋯ ≫ (K.shiftFunctorObjXIso 1 n (n + 1) ⋯).inv))
    (-G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯))
⊢ Eq (α := G.obj ((mappingCone φ).X n) ⟶ G.obj (K.X (n + 1)))
    (G.map (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) n n ⋯))
    (-G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯))

Tactic:
rw [Cochain.rightShift_v _ 1 0 (by lia) n n (by lia) (n + 1) (by lia)]

Premises used: HAdd.hAdd, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ Eq (α := G.obj ((mappingCone φ).X n) ⟶ G.obj (K.X (n + 1)))
    (G.map
      (Cochain.v (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) n (n + 1) ⋯ ≫ (K.shiftFunctorObjXIso 1 n (n + 1) ⋯).inv))
    (-G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯))

Tactic:
simp only [shiftFunctor_obj_X, Cochain.neg_v, shiftFunctorObjXIso,
    HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Functor.map_neg]

Premises used: CochainComplex.HomComplex.Cochain.neg_v, HomologicalComplex.XIsoOfEq_rfl, CochainComplex.shiftFunctor_obj_X, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv, CategoryTheory.Functor.map_neg
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
refine_1 :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L))
    (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ ≫
      𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K) ≫
      CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Triangle.obj₁ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))
      (Triangle.obj₂
        (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))))
    (Triangle.mor₁ (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂
            (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))))
    (Iso.hom
        (Iso.refl
          (Triangle.obj₁
            (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ)))) ≫
      Triangle.mor₁
        (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))

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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L))
    (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ ≫
      𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K) ≫
      CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp