awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
n : ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₃ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
        (Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T)))
    (Triangle.mor₃ (obj (Triangle.shiftFunctor C n ⋙ F.mapTriangle) T) ≫
      map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Iso.app (commShiftIso F n) T.obj₁)))
    (CategoryStruct.comp (Y := Triangle.obj₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T))
      (Iso.hom (Iso.app (commShiftIso F n) T.obj₃)) (Triangle.mor₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D n) T)))
have dsimp : (F.map
        (HSMul.hSMul (β :=
          obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃ ⟶
            obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁))
          n.negOnePow
          (map (shiftFunctor C n) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 n)) T.obj₁ :
            obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₃ ⟶
              obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) T.obj₁)) ≫
    map (shiftFunctor D (A := ℤ) 1) (NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₁) =
  NatTrans.app (Iso.hom (commShiftIso F n)) T.obj₃ ≫
    HSMul.hSMul (β :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₃) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
          (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
      n.negOnePow
      (map (shiftFunctor D n) (F.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) T.obj₁) ≫
          NatTrans.app (Iso.hom (shiftFunctorComm D 1 n)) (F.obj T.obj₁) :
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₃) ⟶
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj T.obj₁)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
⊢ Eq (α :=
    Iso (C := Triangle.{v_1, u_1} C ⥤ Triangle.{v_2, u_2} D) (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle)
      (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)))
    (F.mapTriangleCommShiftIso (n + m)) (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))
have w : ∀ (x : Triangle.{v_1, u_1} C),
  Eq (α :=
    Triangle.obj₁ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
      Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
    (TriangleMorphism.hom₁ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
    (TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
w :
  ∀ (x : Triangle.{v_1, u_1} C),
    Eq (α :=
      Triangle.obj₁ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
        Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
      (TriangleMorphism.hom₁ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
      (TriangleMorphism.hom₁
        (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
⊢ Eq (α :=
    Iso (C := Triangle.{v_1, u_1} C ⥤ Triangle.{v_2, u_2} D) (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle)
      (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)))
    (F.mapTriangleCommShiftIso (n + m)) (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))
have w₁ : ∀ (x : Triangle.{v_1, u_1} C),
  Eq (α :=
    Triangle.obj₂ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
      Triangle.obj₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
    (TriangleMorphism.hom₂ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
    (TriangleMorphism.hom₂
      (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : Preadditive.{v_1, u_1} C
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : F.Additive
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
n m : ℤ
w :
  ∀ (x : Triangle.{v_1, u_1} C),
    Eq (α :=
      Triangle.obj₁ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
        Triangle.obj₁ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
      (TriangleMorphism.hom₁ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
      (TriangleMorphism.hom₁
        (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
w₁ :
  ∀ (x : Triangle.{v_1, u_1} C),
    Eq (α :=
      Triangle.obj₂ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
        Triangle.obj₂ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
      (TriangleMorphism.hom₂ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
      (TriangleMorphism.hom₂
        (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
⊢ Eq (α :=
    Iso (C := Triangle.{v_1, u_1} C ⥤ Triangle.{v_2, u_2} D) (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle)
      (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)))
    (F.mapTriangleCommShiftIso (n + m)) (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))
have w₂ : ∀ (x : Triangle.{v_1, u_1} C),
  Eq (α :=
    Triangle.obj₃ (obj (Triangle.shiftFunctor C (n + m) ⋙ F.mapTriangle) x) ⟶
      Triangle.obj₃ (obj (F.mapTriangle ⋙ Triangle.shiftFunctor D (n + m)) x))
    (TriangleMorphism.hom₃ (NatTrans.app (Iso.hom (F.mapTriangleCommShiftIso (n + m))) x))
    (TriangleMorphism.hom₃
      (NatTrans.app (Iso.hom (CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m))) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : Preadditive.{v_1, u_1} C
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : F.Additive
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_11 : F₁.CommShift ℤ
inst_12 : F₂.CommShift ℤ
inst_13 : NatTrans.CommShift e.hom ℤ
T : Triangle.{v_1, u_1} C
⊢ Eq (α :=
    Triangle.obj₃ (obj F₁.mapTriangle T) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (Triangle.obj₁ (obj F₂.mapTriangle T)))
    (Triangle.mor₃ (obj F₁.mapTriangle T) ≫ map (shiftFunctor D (A := ℤ) 1) (Iso.hom (e.app T.obj₁)))
    (Iso.hom (e.app T.obj₃) ≫ Triangle.mor₃ (obj F₂.mapTriangle T))
have dsimp : Eq (α := F₁.obj T.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F₂.obj T.obj₁))
  ((F₁.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F₁ 1)) T.obj₁) ≫
    map (shiftFunctor D (A := ℤ) 1) (e.hom.app T.obj₁))
  (e.hom.app T.obj₃ ≫ F₂.map T.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F₂ 1)) T.obj₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
Tactic: have h₁ : (0 : X ⟶ Y) = 0 ≫ 𝟙 0 ≫ 0 := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
⊢ Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
have rw : IsZero.{v_2, u_2} (F.obj 0)
Tactic: rw [← IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
⊢ IsZero.{v_2, u_2} (F.obj 0)
have apply : IsIso (X := Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
  (Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
Tactic: apply Triangle.isZero₃_of_isIso₁ _
        (F.map_distinguished _ (contractible_distinguished (0 : C)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
⊢ IsIso (X := Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
    (Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (contractibleTriangle 0)))
have dsimp : IsIso (X := F.obj 0) (F.map (𝟙 0))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
Tactic: have h₂ : 𝟙 (F.obj 0) = 0 := by
      rw [← IsZero.iff_id_eq_zero]
      apply Triangle.isZero₃_of_isIso₁ _
        (F.map_distinguished _ (contractible_distinguished (0 : C)))
      dsimp
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0) ≫ F.map 0)) 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0) ≫ F.map 0)) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw₃ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0) 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0) ≫ F.map 0)) 0
rw₃ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw₄ : Eq (α := F.obj X ⟶ F.obj Y)
  (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) 0 (F.map 0))) 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]