awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
⊢ Eq (α := mappingCone φ₁ ⟶ mappingCone φ₃) (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯ : mappingCone φ₁ ⟶ mappingCone φ₃)
    (CategoryStruct.comp (Y := mappingCone φ₂) (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂)
        (map φ₂ φ₃ a' b' comm' : mappingCone φ₂ ⟶ mappingCone φ₃) :
      mappingCone φ₁ ⟶ mappingCone φ₃)
have h : ∀ (n : ℤ),
  Eq (α := (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
    (HomologicalComplex.Hom.f (map φ₁ φ₃ (a ≫ a') (b ≫ b') sorry) n : (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
    (HomologicalComplex.Hom.f
        (CategoryStruct.comp (Y := mappingCone φ₂) (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂)
          (map φ₂ φ₃ a' b' comm' : mappingCone φ₂ ⟶ mappingCone φ₃))
        n :
      (mappingCone φ₁).X n ⟶ (mappingCone φ₃).X n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ (triangle φ₁).mor₂ ≫ map φ₁ φ₂ a b comm = b ≫ (triangle φ₂).mor₂
have dsimp : Eq (α := L₁ ⟶ mappingCone φ₂)
  (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
      (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂) :
    L₁ ⟶ mappingCone φ₂)
  (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
have rw : Eq (α := L₁ ⟶ mappingCone φ₂)
  (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
      (mapOfHomotopy (Homotopy.ofEq comm) : mappingCone φ₁ ⟶ mappingCone φ₂) :
    L₁ ⟶ mappingCone φ₂)
  (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
Tactic: rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
rw :
  Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (mapOfHomotopy (Homotopy.ofEq comm) : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
⊢ Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (map φ₁ φ₂ a b comm : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)
have rw₁ : Eq (α := L₁ ⟶ mappingCone φ₂) (b ≫ inr φ₂) (b ≫ inr φ₂)
Tactic: rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃
have rw : (triangle φ₁).mor₃ ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
  mapOfHomotopy (Homotopy.ofEq comm) ≫ (triangle φ₂).mor₃
Tactic: rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
rw :
  (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    mapOfHomotopy (Homotopy.ofEq comm) ≫ (triangle φ₂).mor₃
⊢ (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
    map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃
have rw₁ : (triangle φ₁).mor₃ ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a =
  (triangle φ₁).mor₃ ≫
    CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a
Tactic: rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
⊢ CategoryStruct.comp (Y := mappingCone (G := mappingCone φ) (inr φ))
      (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯ :
        Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            K ⟶
          mappingCone (G := mappingCone φ) (inr φ))
      (desc (inr φ) 0 (triangle φ).mor₃ ⋯ :
        mappingCone (G := mappingCone φ) (inr φ) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            K) =
    𝟙 (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K)
have h : ∀ (n : ℤ),
  (CategoryStruct.comp (Y := mappingCone (G := mappingCone φ) (inr φ))
          (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 sorry) (-Cochain.leftShift (inl φ) 1 0 sorry) sorry :
            Functor.obj
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K ⟶
              mappingCone (G := mappingCone φ) (inr φ))
          (desc (inr φ) 0 (triangle φ).mor₃ sorry :
            mappingCone (G := mappingCone φ) (inr φ) ⟶
              Functor.obj
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K)).f
      n =
    HomologicalComplex.Hom.f
      (𝟙
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          K))
      n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
⊢ Cochain.ofHom
      (desc (inr φ) 0 (triangle φ).mor₃ ⋯ ≫
        lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-Cochain.leftShift (inl φ) 1 0 ⋯) ⋯) =
    δ (-1) 0 (-Cochain.comp (snd (inr φ)) (Cochain.comp (snd φ) (inl (inr φ)) ⋯) ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (G := mappingCone φ) (inr φ)))
have h : ∀ (n : ℤ),
  Cochain.v
      (Cochain.ofHom
        (desc (inr φ) 0 (triangle φ).mor₃ sorry ≫
          lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 sorry) (-Cochain.leftShift (inl φ) 1 0 sorry) sorry))
      n n sorry =
    (δ (-1) 0 (-Cochain.comp (snd (inr φ)) (Cochain.comp (snd φ) (inl (inr φ)) sorry) sorry) +
          Cochain.ofHom (𝟙 (mappingCone (G := mappingCone φ) (inr φ)))).v
      n n sorry
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
⊢ 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 φ)))
have h : ∀ (p : ℤ),
  Cochain.v (Cochain.ofHom ((triangle φ).mor₃ ≫ HomotopyEquiv.hom (rotateHomotopyEquiv φ))) p p sorry =
    (HAdd.hAdd (α := Cochain (triangle φ).obj₃ (mappingCone (G := mappingCone φ) (inr φ)) 0)
          (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) sorry)) (Cochain.ofHom (inr (inr φ)))).v
      p p sorry
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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 : ℤ
⊢ 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 ⋯
have 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) sorry))
    p p sorry =
  HAdd.hAdd (α := (mappingCone φ).X p ⟶ (mappingCone (G := mappingCone φ) (inr φ)).X p)
    (Cochain.v (δ (-1) 0 (-Cochain.comp (snd φ) (inl (inr φ)) sorry)) p p sorry) (Cochain.v (Cochain.ofHom (inr (inr φ))) p p sorry)
Tactic: dsimp [rotateHomotopyEquiv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
⊢ HomotopyEquiv.hom (rotateHomotopyEquiv φ) ≫ (triangle (L := mappingCone φ) (inr φ)).mor₃ =
    -CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) φ
have 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
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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 : ℤ
⊢ (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
have h : HomologicalComplex.Hom.f
      (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 triangle._proof_3)
        (-Cochain.leftShift (inl φ) 1 0 rotateHomotopyEquiv._proof_9) sorry)
      p ≫
    (triangle (L := mappingCone φ) (inr φ)).mor₃.f p =
  -φ.f (p + 1)
Tactic: dsimp [rotateHomotopyEquiv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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₃ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangleh φ).rotate.obj₁)) =
    Iso.hom
        (Iso.app (Iso.symm (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K ≪≫
          HomotopyCategory.isoOfHomotopyEquiv (rotateHomotopyEquiv φ)) ≫
      (triangleh (L := mappingCone φ) (inr φ)).mor₃
have dsimp : Eq (α :=
  Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K) ⟶
    Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
  ((-CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ)) ≫
    CategoryTheory.Functor.map
      (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
      (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
  (CategoryStruct.comp (Y :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))
    (CategoryStruct.comp (Y :=
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            K))
        (NatTrans.app (Iso.inv (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (HomotopyEquiv.hom (rotateHomotopyEquiv φ))) :
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K) ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (triangle (L := mappingCone φ) (inr φ)).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) L :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)) ⟶
        Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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 : ℤ
⊢ δ 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
have 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) φ))
            sorry).v
      p q hpq =
    Cochain.v 0 p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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
⊢ (δ 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
have 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) φ))
          sorry).v
      p q hpq =
  0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated (goal)
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 : ℤ
⊢ δ (-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 φ))
have 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 sorry =
    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 sorry
Tactic: ext p