awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  IsZero.{v_1, u_1}
    (Triangle.obj₁.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))
refine_2 : IsZero.{v_1, u_1} (Triangle.obj₁.{v_1, u_1} (Triangle.invRotate (contractibleTriangle (ι.obj X₃))))
refine_3 :
  Triangle.mor₁ (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) =
    Iso.hom (IsZero.iso ⋯ ⋯) ≫ Triangle.mor₁ (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
⊢ Iso (C := Triangle.{v_1, u_1} C) (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0)
    (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
have refine_4 : Triangle.mor₂ (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0) ≫
    Iso.hom
      (Iso.refl
        (Triangle.obj₃.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) =
  Iso.hom
      (Iso.refl
        (Triangle.obj₂.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) ≫
    Triangle.mor₂ (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
Tactic: refine Triangle.isoMk _ _ (IsZero.iso ?_ ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  IsZero.{v_1, u_1}
    (Triangle.obj₁.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))
refine_2 : IsZero.{v_1, u_1} (Triangle.obj₁.{v_1, u_1} (Triangle.invRotate (contractibleTriangle (ι.obj X₃))))
refine_3 :
  Triangle.mor₁ (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) =
    Iso.hom (IsZero.iso ⋯ ⋯) ≫ Triangle.mor₁ (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
refine_4 :
  Triangle.mor₂ (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₃.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₂.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) ≫
      Triangle.mor₂ (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
⊢ Iso (C := Triangle.{v_1, u_1} C) (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0)
    (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
have refine_5 : Triangle.mor₃ (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (IsZero.iso sorry sorry)) =
  Iso.hom
      (Iso.refl
        (Triangle.obj₃.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))) ≫
    Triangle.mor₃ (Triangle.invRotate (contractibleTriangle (ι.obj X₃)))
Tactic: refine Triangle.isoMk _ _ (IsZero.iso ?_ ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
⊢ IsZero.{v_1, u_1}
    (Triangle.obj₁.{v_1, u_1} (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0))
have refine_1 : IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
have refine_1 : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
  (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
have refine_1₁ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
  (Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (ι.obj 0))) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))) 0
refine_1₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (ι.obj 0))) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
have refine_1₂ : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
  (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map (𝟙 0))) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))) 0
refine_1₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (ι.obj 0))) 0
refine_1₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map (𝟙 0))) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
have refine_1₃ : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
  (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))) 0
refine_1₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (ι.obj 0))) 0
refine_1₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map (𝟙 0))) 0
refine_1₃ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map 0)) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
have refine_1₄ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
  (Functor.map (shiftFunctor C (A := ℤ) 1) 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_1 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))) 0
refine_1₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (ι.obj 0))) 0
refine_1₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map (𝟙 0))) 0
refine_1₃ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map 0)) 0
refine_1₄ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
    (Functor.map (shiftFunctor C (A := ℤ) 1) 0) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
have refine_1₅ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj 0))
  0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
⊢ IsZero.{v_1, u_1} (Triangle.obj₁.{v_1, u_1} (Triangle.invRotate (contractibleTriangle (ι.obj X₃))))
have refine_2 : IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
have refine_2 : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
  (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) (ι.map f₂) f₃)
refine_2 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
have refine_2₁ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
  (Functor.map (shiftFunctor C (A := ℤ) (-1)) (𝟙 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]