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 : ℤ
h :
  CategoryStruct.comp (Y :=
      (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
        (lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
            n.negOnePow (Cocycle.shift (fst φ) n))
          (Cochain.shift (snd φ) n) ⋯)
        p)
      (HomologicalComplex.Hom.f
        (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
            n.negOnePow (Cochain.shift (inl φ) n))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯)
        p) =
    𝟙 ((mappingCone φ).X (p + n))
⊢ (CategoryStruct.comp (Y :=
          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) φ))
          (lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
            (HSMul.hSMul (β :=
              Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
              n.negOnePow (Cocycle.shift (fst φ) n))
            (Cochain.shift (snd φ) n) ⋯)
          (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
            (HSMul.hSMul (β :=
              Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
              n.negOnePow (Cochain.shift (inl φ) n))
            (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ))
            ⋯)).f
      p =
    HomologicalComplex.Hom.f
      (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))) 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 : ℤ
⊢ CategoryStruct.comp (Y :=
      (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
        (lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
            n.negOnePow (Cocycle.shift (fst φ) n))
          (Cochain.shift (snd φ) n) ⋯)
        p)
      (HomologicalComplex.Hom.f
        (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
            n.negOnePow (Cochain.shift (inl φ) n))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯)
        p) =
    𝟙 ((mappingCone φ).X (p + n))

Tactic:
simp only [Int.reduceNeg, lift_desc_f _ _ _ _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X',
      Cocycle.coe_units_smul, Cocycle.shift_coe, Cochain.units_smul_v, Cochain.shift_v',
      Linear.comp_units_smul, Linear.units_smul_comp, smul_smul, Int.units_mul_self, one_smul,
      shiftFunctor_map_f', id_X]

Premises used: CochainComplex.HomComplex.Cocycle.coe_units_smul, CategoryTheory.Linear.units_smul_comp, Int.reduceNeg, CochainComplex.mappingCone.id_X, smul_smul, CochainComplex.shiftFunctor_map_f', CategoryTheory.Linear.comp_units_smul, one_smul, CochainComplex.HomComplex.Cochain.units_smul_v, HAdd.hAdd, CochainComplex.HomComplex.Cocycle.shift_coe, CochainComplex.mappingCone.lift_desc_f, CochainComplex.shiftFunctor_obj_X', OfNat.ofNat, CochainComplex.HomComplex.Cochain.shift_v', rfl, Int.units_mul_self
-- 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 : ℤ
h :
  ∀ (p : ℤ),
    HomologicalComplex.Hom.f
        (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
            (HSMul.hSMul (β :=
              Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
              n.negOnePow (Cochain.shift (inl φ) n))
            (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯ ≫
          lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
            (HSMul.hSMul (β :=
              Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
              n.negOnePow (Cocycle.shift (fst φ) n))
            (Cochain.shift (snd φ) n) ⋯)
        p =
      HomologicalComplex.Hom.f
        (𝟙
          (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) φ)))
        p
⊢ desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
        (HSMul.hSMul (β :=
          Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
          n.negOnePow (Cochain.shift (inl φ) n))
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯ ≫
      lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
        (HSMul.hSMul (β :=
          Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
          n.negOnePow (Cocycle.shift (fst φ) n))
        (Cochain.shift (snd φ) 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) φ))

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 : ℤ
h :
  HomologicalComplex.Hom.f
        (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
            n.negOnePow (Cochain.shift (inl φ) n))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯)
        p ≫
      HomologicalComplex.Hom.f
        (lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
            n.negOnePow (Cocycle.shift (fst φ) n))
          (Cochain.shift (snd φ) n) ⋯)
        p =
    𝟙
      ((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
      (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
            n.negOnePow (Cochain.shift (inl φ) n))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯ ≫
        lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
            n.negOnePow (Cocycle.shift (fst φ) n))
          (Cochain.shift (snd φ) n) ⋯)
      p =
    HomologicalComplex.Hom.f
      (𝟙
        (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) φ)))
      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 : ℤ
⊢ HomologicalComplex.Hom.f
        (desc (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K)
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ)) (-1))
            n.negOnePow (Cochain.shift (inl φ) n))
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)) ⋯)
        p ≫
      HomologicalComplex.Hom.f
        (lift (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ)
          (HSMul.hSMul (β :=
            Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K) 1)
            n.negOnePow (Cocycle.shift (fst φ) n))
          (Cochain.shift (snd φ) n) ⋯)
        p =
    𝟙
      ((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 [Int.reduceNeg, ext_from_iff _ (p + 1) _ rfl, shiftFunctor_obj_X',
      inl_v_desc_f_assoc, Cochain.units_smul_v, Cochain.shift_v', Linear.units_smul_comp, comp_id,
      ext_to_iff _ _ (p + 1) rfl, assoc, lift_f_fst_v,
      Cocycle.coe_units_smul, Cocycle.shift_coe, Linear.comp_units_smul, inl_v_fst_v, smul_smul,
      Int.units_mul_self, one_smul, lift_f_snd_v, inl_v_snd_v, smul_zero, and_self,
      inr_f_desc_f_assoc, shiftFunctor_map_f', inr_f_fst_v, inr_f_snd_v]

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.HomComplex.Cocycle.coe_units_smul, and_self, CategoryTheory.Linear.units_smul_comp, CochainComplex.mappingCone.lift_f_fst_v, Int.reduceNeg, smul_zero, smul_smul, CochainComplex.mappingCone.ext_from_iff, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.shiftFunctor_map_f', CochainComplex.mappingCone.ext_to_iff, CochainComplex.mappingCone.inl_v_desc_f_assoc, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Category.comp_id, one_smul, CochainComplex.mappingCone.inl_v_fst_v, CochainComplex.HomComplex.Cochain.units_smul_v, HAdd.hAdd, CochainComplex.HomComplex.Cocycle.shift_coe, CochainComplex.shiftFunctor_obj_X', CochainComplex.mappingCone.inl_v_snd_v, CochainComplex.mappingCone.lift_f_snd_v, OfNat.ofNat, CochainComplex.HomComplex.Cochain.shift_v', rfl, CochainComplex.mappingCone.inr_f_desc_f_assoc, Int.units_mul_self
-- 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_1 :
  (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₁ ≫
      (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 =
    Iso.hom (Iso.refl (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₁) ≫
      (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₁
refine_2 :
  (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₂ ≫
      Iso.hom (shiftIso φ n) =
    (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₂
refine_3 :
  (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₃
⊢ Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ) ≅
    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) φ)

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (n.negOnePow • Iso.refl _) (shiftIso φ n) ?_ ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, HSMul.hSMul, Int.negOnePow
-- 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_1 :
  HSMul.hSMul (β :=
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K ⟶
          Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)
        n.negOnePow (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ) ≫
      HSMul.hSMul (β :=
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L ⟶
          Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)
        n.negOnePow (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)) =
    𝟙 (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) φ
⊢ (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₁ ≫
      (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 =
    Iso.hom (Iso.refl (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).obj₁) ≫
      (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:
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 : ℤ
⊢ HSMul.hSMul (β :=
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K ⟶
          Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)
        n.negOnePow (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ) ≫
      HSMul.hSMul (β :=
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L ⟶
          Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)
        n.negOnePow (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) L)) =
    𝟙 (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) φ

Tactic:
simp only [Linear.comp_units_smul, comp_id, id_comp, smul_smul,
      Int.units_mul_self, one_smul]

Premises used: smul_smul, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Category.comp_id, one_smul, CategoryTheory.Category.id_comp, Int.units_mul_self
-- 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_2 :
  ∀ (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
⊢ (Functor.obj (Triangle.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (triangle φ)).mor₂ ≫
      Iso.hom (shiftIso φ n) =
    (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₂

Tactic:
ext p