awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ
⊢ 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 φ))
have 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) sorry)
          (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 φ))
            sorry)).f
      p =
    HomologicalComplex.Hom.f
      (𝟙 (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) (mappingCone φ))) p
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
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) φ))
          (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
have 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) sorry)
      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 φ)) sorry)
      p) =
  𝟙 ((mappingCone φ).X (p + n))
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 : ℤ
⊢ 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) φ))
have 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 φ)) sorry ≫
        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) sorry)
      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: 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
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 φ)) ⋯ ≫
        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
have 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 φ)) sorry)
      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) sorry)
      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: 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 : ℤ
⊢ 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) φ)
have 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₁
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) (n.negOnePow • Iso.refl _) (shiftIso φ 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
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₁
⊢ 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) φ)
have 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₂
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) (n.negOnePow • Iso.refl _) (shiftIso φ 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
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₂
⊢ 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) φ)
have 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₃
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) (n.negOnePow • Iso.refl _) (shiftIso φ 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
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₁
have 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) φ
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 : ℤ
⊢ (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₂
have 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
Tactic: ext p