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
h :
  ∀ (p : ℤ),
    Cochain.v (Cochain.ofHom ((triangle φ).mor₃ ≫ HomotopyEquiv.hom (rotateHomotopyEquiv φ))) p p ⋯ =
      (HAdd.hAdd (α := Cochain (triangle φ).obj₃ (mappingCone (G := mappingCone φ) (inr φ)) 0)
            (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) ⋯)) (Cochain.ofHom (inr (inr φ)))).v
        p p ⋯
⊢ Cochain.ofHom ((triangle φ).mor₃ ≫ HomotopyEquiv.hom (rotateHomotopyEquiv φ)) =
    HAdd.hAdd (α := Cochain (triangle φ).obj₃ (mappingCone (G := mappingCone φ) (inr φ)) 0)
      (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) ⋯)) (Cochain.ofHom (inr (inr φ)))

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
p : ℤ
h :
  Cochain.v
      (Cochain.ofHom
        ((triangle φ).mor₃ ≫
          lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
            (-Cochain.leftShift (inl φ) 1 0 rotateHomotopyEquiv._proof_9) ⋯))
      p p ⋯ =
    HAdd.hAdd (α := (mappingCone φ).X p ⟶ (mappingCone (G := mappingCone φ) (inr φ)).X p)
      (Cochain.v (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) ⋯)) p p ⋯)
      (Cochain.v (Cochain.ofHom (inr (inr φ))) p p ⋯)
⊢ Cochain.v (Cochain.ofHom ((triangle φ).mor₃ ≫ HomotopyEquiv.hom (rotateHomotopyEquiv φ))) p p ⋯ =
    (HAdd.hAdd (α := Cochain (triangle φ).obj₃ (mappingCone (G := mappingCone φ) (inr φ)) 0)
          (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) ⋯)) (Cochain.ofHom (inr (inr φ)))).v
      p p ⋯

Tactic:
dsimp [rotateHomotopyEquiv]

Premises used: CochainComplex.mappingCone.rotateHomotopyEquiv
-- 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
p : ℤ
⊢ p + 1 + -1 = p

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
p : ℤ
⊢ p + 1 + 0 = p + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ).obj₃ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ).mor₃ ≫
        CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (HomotopyEquiv.hom (rotateHomotopyEquiv φ)) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (triangle φ).obj₃ ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr (inr φ)) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ) ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))

Tactic:
simpa only [Functor.map_comp]
    using HomotopyCategory.eq_of_homotopy _ _ (rotateHomotopyEquivComm₂Homotopy φ)

Premises used: CochainComplex.mappingCone.rotateHomotopyEquivComm₂Homotopy, HomotopyCategory.eq_of_homotopy, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
h :
  ∀ (p : ℤ),
    (HomotopyEquiv.hom (rotateHomotopyEquiv φ) ≫ (triangle (L := mappingCone φ) (inr φ)).mor₃).f p =
      HomologicalComplex.Hom.f
        (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) φ) p
⊢ HomotopyEquiv.hom (rotateHomotopyEquiv φ) ≫ (triangle (L := mappingCone φ) (inr φ)).mor₃ =
    -CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) φ

Tactic:
ext p
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
h :
  HomologicalComplex.Hom.f
        (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
          (-Cochain.leftShift (inl φ) 1 0 rotateHomotopyEquiv._proof_9) ⋯)
        p ≫
      (triangle (L := mappingCone φ) (inr φ)).mor₃.f p =
    -φ.f (p + 1)
⊢ (HomotopyEquiv.hom (rotateHomotopyEquiv φ) ≫ (triangle (L := mappingCone φ) (inr φ)).mor₃).f p =
    HomologicalComplex.Hom.f
      (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) φ) p

Tactic:
dsimp [rotateHomotopyEquiv]

Premises used: CochainComplex.mappingCone.rotateHomotopyEquiv
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
⊢ p + 1 + 0 = p + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
⊢ HomologicalComplex.Hom.f
        (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
          (-Cochain.leftShift (inl φ) 1 0 rotateHomotopyEquiv._proof_9) ⋯)
        p ≫
      (triangle (L := mappingCone φ) (inr φ)).mor₃.f p =
    -φ.f (p + 1)

Tactic:
simp only [Int.reduceNeg, lift_f _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X', Cocycle.coe_neg,
    Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.neg_v,
    (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia),
    shiftFunctor_obj_X, mul_one, sub_self, mul_zero, Int.zero_ediv, add_zero, Int.negOnePow_one,
    shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Cochain.ofHom_v, id_comp,
    Units.neg_smul, one_smul, neg_neg, Preadditive.neg_comp, Preadditive.add_comp, assoc,
    inl_v_triangle_mor₃_f, Iso.refl_inv, Preadditive.comp_neg, comp_id, inr_f_triangle_mor₃_f,
    comp_zero, neg_zero]

Premises used: CategoryTheory.Category.assoc, sub_self, CochainComplex.HomComplex.Cochain.neg_v, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctor_obj_X, CochainComplex.HomComplex.Cocycle.coe_neg, neg_neg, CochainComplex.HomComplex.Cochain.ofHom_v, Int.negOnePow_one, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, zero_add, one_smul, MulZeroClass.mul_zero, CategoryTheory.Preadditive.add_comp, CochainComplex.HomComplex.Cochain.ofHom, CategoryTheory.Iso.refl_inv, Units.neg_smul, HAdd.hAdd, Int.zero_ediv, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.shiftFunctor_obj_X', CategoryTheory.Preadditive.neg_comp, CochainComplex.HomComplex.Cocycle.ofHom_coe, mul_one, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cocycle.leftShift_coe, neg_zero, CategoryTheory.Iso.refl_hom, CochainComplex.mappingCone.lift_f, rfl, 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
⊢ (triangleh φ).rotate.mor₁ ≫ Iso.hom (Iso.refl (triangleh φ).rotate.obj₂) =
    Iso.hom (Iso.refl (triangleh φ).rotate.obj₁) ≫ (triangleh (L := mappingCone φ) (inr φ)).mor₁

Tactic:
simp
-- 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
⊢ (triangleh φ).rotate.mor₂ ≫
      Iso.hom
        (Iso.app (Iso.symm (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K ≪≫
          HomotopyCategory.isoOfHomotopyEquiv (rotateHomotopyEquiv φ)) =
    Iso.hom (Iso.refl (triangleh φ).rotate.obj₂) ≫ (triangleh (L := mappingCone φ) (inr φ)).mor₂

Tactic:
simp
-- 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 q : ℤ) (hpq : p + 1 = q),
    (δ 0 1 (Cochain.shift (snd φ) 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 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))
                    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) 1).comp
              (Cochain.ofHom
                (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ))
              ⋯).v
        p q hpq =
      Cochain.v 0 p q hpq
⊢ δ 0 1 (Cochain.shift (snd φ) 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 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) 1).comp
        (Cochain.ofHom
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ))
        ⋯ =
    0

Tactic:
ext p q hpq
-- 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 q : ℤ
hpq : p + 1 = q
h :
  Cochain.v (δ 0 1 (Cochain.shift (snd φ) n)) p q hpq +
      ((HSMul.hSMul (β :=
                Cochain (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 (Cochain.shift (↑(fst φ) : Cochain (mappingCone φ) K 1) n)).comp
            (Cochain.ofHom
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ))
            ⋯).v
        p q hpq =
    0
⊢ (δ 0 1 (Cochain.shift (snd φ) 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 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))
                  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) 1).comp
            (Cochain.ofHom
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ))
            ⋯).v
      p q hpq =
    Cochain.v 0 p q hpq

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 q : ℤ
hpq : p + 1 = q
⊢ Cochain.v (δ 0 1 (Cochain.shift (snd φ) n)) p q hpq +
      ((HSMul.hSMul (β :=
                Cochain (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 (Cochain.shift (↑(fst φ) : Cochain (mappingCone φ) K 1) n)).comp
            (Cochain.ofHom
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ))
            ⋯).v
        p q hpq =
    0

Tactic:
simp only [Cochain.δ_shift, δ_snd, Cochain.shift_neg, smul_neg, Cochain.neg_v,
      shiftFunctor_obj_X', Cochain.units_smul_v, Cochain.shift_v', Cochain.comp_zero_cochain_v,
      Cochain.ofHom_v, Cochain.units_smul_comp, shiftFunctor_map_f', neg_add_cancel]

Premises used: CochainComplex.HomComplex.Cochain.units_smul_comp, CochainComplex.HomComplex.Cochain.shift_neg, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CochainComplex.HomComplex.Cochain.neg_v, smul_neg, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.shiftFunctor_map_f', CochainComplex.mappingCone.δ_snd, CochainComplex.HomComplex.Cochain.units_smul_v, neg_add_cancel, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftFunctor_obj_X', CochainComplex.HomComplex.Cochain.shift_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
n : ℤ
h :
  ∀ (p : ℤ),
    Cochain.v
        (δ (-1) 0
          (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)))
        p p ⋯ =
      Cochain.v
        (Cochain.ofHom
          (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ ≫
            CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)))
        p p ⋯
⊢ δ (-1) 0
      (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)) =
    Cochain.ofHom
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ ≫
        CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ))

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 :
  Cochain.v
      (δ (-1) 0
        (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)))
      p p ⋯ =
    Cochain.v
      (Cochain.ofHom
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)))
      p p ⋯
⊢ Cochain.v
      (δ (-1) 0
        (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)))
      p p ⋯ =
    Cochain.v
      (Cochain.ofHom
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)))
      p 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 : ℤ
⊢ Cochain.v
      (δ (-1) 0
        (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)))
      p p ⋯ =
    Cochain.v
      (Cochain.ofHom
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) φ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (inr φ)))
      p p ⋯

Tactic:
simp only [Int.reduceNeg, δ_units_smul, Cochain.δ_shift, δ_inl, Cochain.ofHom_comp, smul_smul,
      Int.units_mul_self, one_smul, Cochain.shift_v', Cochain.comp_zero_cochain_v,
      Cochain.ofHom_v, shiftFunctor_obj_X', shiftFunctor_map_f']

Premises used: CochainComplex.HomComplex.δ_units_smul, CochainComplex.mappingCone.δ_inl, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, Int.reduceNeg, smul_smul, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.shiftFunctor_map_f', one_smul, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftFunctor_obj_X', CochainComplex.HomComplex.Cochain.shift_v', Int.units_mul_self, CochainComplex.HomComplex.Cochain.ofHom_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 : ℤ
h :
  ∀ (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) φ))
            (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
⊢ 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 φ)) ⋯) =
    𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))

Tactic:
ext p