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
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
h₂ : IsZero.{v, u} T.obj₂
h₃ : IsZero.{v, u} T.obj₃
⊢ IsZero.{v, u} T.obj₁
have rw : T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: rw [T.isZero₁_iff 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₁ : IsZero.{v, u} T.obj₁
h₃ : IsZero.{v, u} T.obj₃
⊢ IsZero.{v, u} T.obj₂
have rw : T.mor₁ = 0 ∧ T.mor₂ = 0
Tactic: rw [T.isZero₂_iff 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₁ : IsZero.{v, u} T.obj₁
h₂ : IsZero.{v, u} T.obj₂
⊢ IsZero.{v, u} T.rotate.obj₃
have dsimp : IsZero.{v, u} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
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
h₁ : IsZero.{v, u} T.obj₁
h₂ : IsZero.{v, u} T.obj₂
⊢ IsZero.{v, u} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
have simp : ∀ (h₁ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₁) (𝟙 T.obj₁) 0),
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)) 0
Tactic: simp only [IsZero.iff_id_eq_zero] at h₁ ⊢
Cleared hypotheses: h₁
-- 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₂ : IsZero.{v, u} T.obj₂
h₁ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₁) (𝟙 T.obj₁) 0
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)) 0
have rw : Eq.{v + 1} (α :=
  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
  (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁)) 0
Tactic: rw [← Functor.map_id, h₁, Functor.map_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₂ : IsZero.{v, u} T.obj₂
h₁ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₁) (𝟙 T.obj₁) 0
rw :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁)) 0
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)) 0
have rw₁ : Eq.{v + 1} (α :=
  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
  (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) 0) 0
Tactic: rw [← Functor.map_id, h₁, Functor.map_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₂ : IsZero.{v, u} T.obj₂
h₁ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₁) (𝟙 T.obj₁) 0
rw :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁)) 0
rw₁ :
  Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) 0) 0
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
    (𝟙 (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)) 0
have rw₂ : Eq.{v + 1} (α :=
  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁)
  0 0
Tactic: rw [← Functor.map_id, h₁, Functor.map_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₁ ↔ IsIso T.mor₂
have rw : T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂
Tactic: rw [T.isZero₁_iff 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
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂
have mp : T.mor₁ = 0 ∧ T.mor₃ = 0 → IsIso 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 ∧ T.mor₃ = 0 → IsIso T.mor₂
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂
have mpr : IsIso T.mor₂ → T.mor₁ = 0 ∧ T.mor₃ = 0
Tactic: constructor
-- 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
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
⊢ IsIso T.mor₂
have this : Epi T.mor₂
Tactic: have := T.epi₂ hT h₃
-- 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
this : Epi T.mor₂
⊢ T.mor₁ ≫ 𝟙 T.obj₂ = 0
have rw : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₂) (0 ≫ 𝟙 T.obj₂) 0
Tactic: rw [h₁, 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₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
rw : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₂) (0 ≫ 𝟙 T.obj₂) 0
⊢ T.mor₁ ≫ 𝟙 T.obj₂ = 0
have rw₁ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₂) 0 0
Tactic: rw [h₁, 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₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
⊢ IsIso T.mor₂
have mp : ∀ (f : T.obj₃ ⟶ T.obj₂) (hf : 𝟙 T.obj₂ = T.mor₂ ≫ f), IsIso T.mor₂
Tactic: obtain ⟨f, hf⟩ := yoneda_exact₂ T hT (𝟙 _) (by rw [h₁, 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₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
⊢ f ≫ T.mor₂ = 𝟙 T.obj₃
have rw : T.mor₂ ≫ f ≫ T.mor₂ = T.mor₂ ≫ 𝟙 T.obj₃
Tactic: rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]
-- 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
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
rw : T.mor₂ ≫ f ≫ T.mor₂ = T.mor₂ ≫ 𝟙 T.obj₃
⊢ f ≫ T.mor₂ = 𝟙 T.obj₃
have rw₁ : T.mor₂ ≫ f ≫ T.mor₂ = T.mor₂
Tactic: rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]
-- 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
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
rw : T.mor₂ ≫ f ≫ T.mor₂ = T.mor₂ ≫ 𝟙 T.obj₃
rw₁ : T.mor₂ ≫ f ≫ T.mor₂ = T.mor₂
⊢ f ≫ T.mor₂ = 𝟙 T.obj₃
have rw₂ : T.mor₂ = T.mor₂
Tactic: rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]
-- 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 : IsIso T.mor₂
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0
have mpr : Mono T.mor₂ ∧ Epi T.mor₂
Tactic: rw [T.mor₁_eq_zero_iff_mono₂ hT, T.mor₃_eq_zero_iff_epi₂ 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 : IsIso T.mor₂
⊢ Mono T.mor₂ ∧ Epi T.mor₂
have mpr : 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
h : IsIso T.mor₂
mpr : Mono T.mor₂
⊢ Mono T.mor₂ ∧ Epi T.mor₂
have mpr₁ : Epi 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
⊢ IsZero.{v, u} T.obj₃ ↔ IsIso T.mor₁
have refine : IsZero.{v, u} T.obj₃ ↔ IsZero.{v, u} T.invRotate.obj₁
Tactic: refine Iff.trans ?_ (Triangle.isZero₁_iff_isIso₂ _ (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
⊢ IsZero.{v, u} T.obj₃ ↔ IsZero.{v, u} T.invRotate.obj₁
have dsimp : IsZero.{v, u} T.obj₃ ↔ IsZero.{v, u} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃)
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
n : ℤ
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Functor.obj (CategoryTheory.shiftFunctor (Triangle.{v, u} C) n) T)
have revert : ∀ (T : Triangle.{v, u} C)
  (hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T),
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Functor.obj (CategoryTheory.shiftFunctor (Triangle.{v, u} C) n) T)
Tactic: revert T hT
Cleared hypotheses: T, 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
n : ℤ
H : ℤ → Prop :=
  fun (n : ℤ) ↦
    ∀ (T : Triangle.{v, u} C),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T →
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Functor.obj (shiftFunctor C n) T)
⊢ ∀ (T : Triangle.{v, u} C)
    (hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Functor.obj (CategoryTheory.shiftFunctor (Triangle.{v, u} C) n) T)
have change : H n
Tactic: change H n