awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.mor₁ = 0 ↔ Mono T.mor₂
have mp : T.mor₁ = 0 → Mono T.mor₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₁ = 0 → Mono T.mor₂
⊢ T.mor₁ = 0 ↔ Mono T.mor₂
have mpr : Mono T.mor₂ → T.mor₁ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₁ = 0
⊢ Mono T.mor₂
have mp : ∀ (P : C) (g : P ⟶ T.obj₂), g ≫ T.mor₂ = 0 → g = 0
Tactic: rw [mono_iff_cancel_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₁ = 0
X : C
g : X ⟶ T.obj₂
hg : g ≫ T.mor₂ = 0
⊢ g = 0
have mp : ∀ (f : X ⟶ T.obj₁) (hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0), f ≫ T.mor₁ = 0
Tactic: obtain ⟨f, rfl⟩ := coyoneda_exact₂ T hT g hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₁ = 0
X : C
f : X ⟶ T.obj₁
hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0
⊢ f ≫ T.mor₁ = 0
have mp : Eq (α := X ⟶ T.obj₂) (f ≫ 0) 0
Tactic: rw [h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : T.mor₁ = 0
X : C
f : X ⟶ T.obj₁
hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0
mp : Eq (α := X ⟶ T.obj₂) (f ≫ 0) 0
⊢ f ≫ T.mor₁ = 0
have mp₁ : Eq.{v + 1} (α := X ⟶ T.obj₂) 0 0
Tactic: rw [h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : Mono T.mor₂
⊢ T.mor₁ = 0
have mpr : T.mor₁ ≫ T.mor₂ = 0 ≫ T.mor₂
Tactic: rw [← cancel_mono T.mor₂, comp_distTriang_mor_zero₁₂ _ hT, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : Mono T.mor₂
mpr : T.mor₁ ≫ T.mor₂ = 0 ≫ T.mor₂
⊢ T.mor₁ = 0
have mpr₁ : Eq (α := T.obj₁ ⟶ T.obj₃) 0 (0 ≫ T.mor₂)
Tactic: rw [← cancel_mono T.mor₂, comp_distTriang_mor_zero₁₂ _ hT, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : Mono T.mor₂
mpr : T.mor₁ ≫ T.mor₂ = 0 ≫ T.mor₂
mpr₁ : Eq (α := T.obj₁ ⟶ T.obj₃) 0 (0 ≫ T.mor₂)
⊢ T.mor₁ = 0
have mpr₂ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₃) 0 0
Tactic: rw [← cancel_mono T.mor₂, comp_distTriang_mor_zero₁₂ _ hT, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.mor₃ = 0 ↔ Mono T.mor₁
have h : T.invRotate.mor₁ = 0 ↔ Mono T.invRotate.mor₂
Tactic: have h := mor₁_eq_zero_iff_mono₂ _ (inv_rot_of_distTriang _ hT)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h :
  Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ↔
    Mono T.mor₁
⊢ T.mor₃ = 0 ↔ Mono T.mor₁
have rw : T.mor₃ = 0 ↔
  Eq (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1))
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁))
    (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃) 0
Tactic: rw [← h, neg_eq_zero, IsIso.comp_right_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ IsZero.{v, u} T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0
have mp : IsZero.{v, u} T.obj₂ → T.mor₁ = 0 ∧ T.mor₂ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : IsZero.{v, u} T.obj₂ → T.mor₁ = 0 ∧ T.mor₂ = 0
⊢ IsZero.{v, u} T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0
have mpr : T.mor₁ = 0 ∧ T.mor₂ = 0 → IsZero.{v, u} T.obj₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
⊢ 𝟙 T.obj₂ ≫ T.mor₂ = 0
have rw : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₃) (𝟙 T.obj₂ ≫ 0) 0
Tactic: rw [h₂, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
rw : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₃) (𝟙 T.obj₂ ≫ 0) 0
⊢ 𝟙 T.obj₂ ≫ T.mor₂ = 0
have rw₁ : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₃) 0 0
Tactic: rw [h₂, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
⊢ IsZero.{v, u} T.obj₂
have mpr : ∀ (f : T.obj₂ ⟶ T.obj₁) (hf : 𝟙 T.obj₂ = f ≫ T.mor₁), IsZero.{v, u} T.obj₂
Tactic: obtain ⟨f, hf⟩ := coyoneda_exact₂ T hT (𝟙 _) (by rw [h₂, comp_zero])
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
f : T.obj₂ ⟶ T.obj₁
hf : 𝟙 T.obj₂ = f ≫ T.mor₁
⊢ IsZero.{v, u} T.obj₂
have mpr : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) (𝟙 T.obj₂) 0
Tactic: rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
f : T.obj₂ ⟶ T.obj₁
hf : 𝟙 T.obj₂ = f ≫ T.mor₁
mpr : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) (𝟙 T.obj₂) 0
⊢ IsZero.{v, u} T.obj₂
have mpr₁ : f ≫ T.mor₁ = 0
Tactic: rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
f : T.obj₂ ⟶ T.obj₁
hf : 𝟙 T.obj₂ = f ≫ T.mor₁
mpr : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) (𝟙 T.obj₂) 0
mpr₁ : f ≫ T.mor₁ = 0
⊢ IsZero.{v, u} T.obj₂
have mpr₂ : Eq (α := T.obj₂ ⟶ T.obj₂) (f ≫ 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h₁ : T.mor₁ = 0
h₂ : T.mor₂ = 0
f : T.obj₂ ⟶ T.obj₁
hf : 𝟙 T.obj₂ = f ≫ T.mor₁
mpr : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) (𝟙 T.obj₂) 0
mpr₁ : f ≫ T.mor₁ = 0
mpr₂ : Eq (α := T.obj₂ ⟶ T.obj₂) (f ≫ 0) 0
⊢ IsZero.{v, u} T.obj₂
have mpr₃ : Eq.{v + 1} (α := T.obj₂ ⟶ T.obj₂) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, hf, h₁, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ IsZero.{v, u} T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have refine : T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: refine (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have dsimp : Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
      (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ∧
    T.mor₁ = 0 ↔
  T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ Eq (α := Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
        (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁ :
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶ T.obj₁)
        (0 : T.invRotate.obj₁ ⟶ T.invRotate.obj₂) ∧
      T.mor₁ = 0 ↔
    T.mor₁ = 0 ∧ T.mor₃ = 0
have simp : T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mp₁ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mp₁ mp₂ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mp₃ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mp₁ mp₂ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mp₃ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mp₄ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₃ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mp₁ mp₂ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mp₃ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0
mp₄ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₃ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mpr₁ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mp₁ mp₂ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mp₃ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0
mp₄ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₃ = 0
mpr₁ mpr₂ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mpr₃ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : T.mor₃ = 0 ∧ T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mpr : T.mor₁ = 0 ∧ T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mp₁ mp₂ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0 ∧ T.mor₃ = 0
mp₃ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₁ = 0
mp₄ : T.mor₃ = 0 → T.mor₁ = 0 → T.mor₃ = 0
mpr₁ mpr₂ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0 ∧ T.mor₁ = 0
mpr₃ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₃ = 0
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
have mpr₄ : T.mor₁ = 0 → T.mor₃ = 0 → T.mor₁ = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ IsZero.{v, u} T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
have refine : T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
Tactic: refine (isZero₂_iff _ (rot_of_distTriang _ hT)).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
have dsimp : T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.mor₂ = 0 ∧ T.mor₃ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
have mp : T.mor₂ = 0 ∧ T.mor₃ = 0 → T.mor₂ = 0 ∧ T.mor₃ = 0
Tactic: tauto