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 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
have 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)
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₃ ≫
      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₃
have 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
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 : ℤ
⊢ ((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
have 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
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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
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)
have 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) sorry) ≫
        Cochain.v (inl (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) (n + 1) n sorry)
      (G.map (Cochain.v (snd φ) n n sorry) ≫
        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: rw [mapHomologicalComplexXIso_eq φ G n (n + 1) rfl, mapHomologicalComplexXIso'_hom]
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ 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
have h : G.map ((triangle φ).mor₃.f n) = -G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) sorry)
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]
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) = -G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) ⋯)
have 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 sorry))
  (-G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) sorry))
Tactic: dsimp [triangle]
-- 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
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 (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) ⋯))
have 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) sorry ≫ (K.shiftFunctorObjXIso 1 n (n + 1) sorry).inv))
  (-G.map (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) K 1) n (n + 1) sorry))
Tactic: rw [Cochain.rightShift_v _ 1 0 (by lia) n n (by lia) (n + 1) (by lia)]
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
⊢ Iso (C := Triangle (HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ)))
    (Functor.obj (Functor.mapTriangle (G.mapHomologicalComplex (ComplexShape.up ℤ))) (triangle φ))
    (triangle (K := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
have refine_1 : 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: refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (mapHomologicalComplexIso φ G) ?_ ?_ ?_
-- 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
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 ℤ))
      (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 ℤ)) φ)))
have 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 ℤ)) φ)
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
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 ℤ)) L)
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (CategoryStruct.comp (Y := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
        (Iso.hom (mapHomologicalComplexIso φ G)) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L) ≫
        inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
have refine_2 : Eq (α :=
  Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
    (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
    (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
  (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
  (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L) ≫
    inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
Tactic: rw [map_inr, id_comp]
-- 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
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
refine_2 :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L) ≫
      inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (CategoryStruct.comp (Y := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
        (Iso.hom (mapHomologicalComplexIso φ G)) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L) ≫
        inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
have refine_2₁ : Eq (α :=
  Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
    (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
    (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
      (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
  (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
  (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
Tactic: rw [map_inr, id_comp]
-- 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
T₁ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT₁ :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₁
T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₂
have obtain : ∀ (X Y : CochainComplex.{v_1, u_1, 0} C ℤ) (f : X ⟶ Y) (e' : T₁ ≅ CochainComplex.mappingCone.triangleh f),
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₂
Tactic: obtain ⟨X, Y, f, ⟨e'⟩⟩ := hT₁
Cleared hypotheses: hT₁
-- 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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (contractibleTriangle X)
have obtain : ∀ (X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)),
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
Tactic: obtain ⟨X⟩ := X
Cleared hypotheses: X
-- 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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
have refine : contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X) ≅
  CochainComplex.mappingCone.triangleh (𝟙 X)
Tactic: refine ⟨_, _, 𝟙 X, ⟨?_⟩⟩