awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
rw₂ 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
⊢ 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:
rw [← Functor.map_id, h₁, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
rw : T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂
⊢ IsZero.{v, u} T.obj₁ ↔ IsIso T.mor₂

Tactic:
rw [T.isZero₁_iff hT]

Premises used: CategoryTheory.Pretriangulated.Triangle.isZero₁_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂
mpr : IsIso T.mor₂ → T.mor₁ = 0 ∧ T.mor₃ = 0
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
⊢ Epi T.mor₂

Tactic:
have := T.epi₂ hT h₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
rw₁ rw₂ : Eq.{v + 1} (α := T.obj₁ ⟶ T.obj₂) 0 0
⊢ T.mor₁ ≫ 𝟙 T.obj₂ = 0

Tactic:
rw [h₁, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂
mp : ∀ (f : T.obj₃ ⟶ T.obj₂) (hf : 𝟙 T.obj₂ = T.mor₂ ≫ f), IsIso T.mor₂
⊢ IsIso T.mor₂

Tactic:
obtain ⟨f, hf⟩ := yoneda_exact₂ T hT (𝟙 _) (by rw [h₁, zero_comp])

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂
rw₂ rw₃ : T.mor₂ = T.mor₂
⊢ f ≫ T.mor₂ = 𝟙 T.obj₃

Tactic:
rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Pretriangulated.Triangle.mor₂, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
⊢ IsIso T.mor₂

Tactic:
exact ⟨f, hf.symm, by rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂ ∧ Epi T.mor₂
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
rw [T.mor₁_eq_zero_iff_mono₂ hT, T.mor₃_eq_zero_iff_epi₂ hT]

Premises used: CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂
mpr₁ : Epi T.mor₂
⊢ Mono T.mor₂ ∧ Epi T.mor₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂
⊢ Epi T.mor₂

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₃

Tactic:
isZero₁_iff_isIso₂ _ (rot_of_distTriang _ hT)

Premises used: CategoryTheory.Pretriangulated.rot_of_distTriang, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₁

Tactic:
Iff.trans ?_ (Triangle.isZero₁_iff_isIso₂ _ (inv_rot_of_distTriang _ hT))

Premises used: CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Iff.trans, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
refine : IsZero.{v, u} T.obj₃ ↔ IsZero.{v, u} T.invRotate.obj₁
⊢ IsZero.{v, u} T.obj₃ ↔ IsIso T.mor₁

Tactic:
refine Iff.trans ?_ (Triangle.isZero₁_iff_isIso₂ _ (inv_rot_of_distTriang _ hT))

Premises used: CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Iff.trans, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
dsimp :
  IsZero.{v, u} T.obj₃ ↔ IsZero.{v, u} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃)
⊢ IsZero.{v, u} T.obj₃ ↔ IsZero.{v, u} T.invRotate.obj₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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} (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) (-1)) T.obj₃)

Tactic:
simp only [IsZero.iff_id_eq_zero, ← Functor.map_id, Functor.map_eq_zero_iff]

Premises used: CategoryTheory.Functor.map_eq_zero_iff, CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₂
⊢ IsZero.{v, u} T.obj₁

Tactic:
(T.isZero₁_iff_isIso₂ hT).2 h

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₃
⊢ IsZero.{v, u} T.obj₂

Tactic:
(T.isZero₂_iff_isIso₃ hT).2 h

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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₁
⊢ IsZero.{v, u} T.obj₃

Tactic:
(T.isZero₃_iff_isIso₁ hT).2 h

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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 : ℤ
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)
⊢ 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
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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)
change : H n
⊢ ∀ (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:
change H n
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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)
have : ∀ (H_zero : H 0), H n
⊢ H n

Tactic:
have H_zero : H 0 := fun T hT =>
    isomorphic_distinguished _ hT _ ((Triangle.shiftFunctorZero C).app T)
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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)
H_zero : H 0
⊢ H 1

Tactic:
have H_one : H 1 := fun T hT =>
    isomorphic_distinguished _ (rot_of_distTriang _
      (rot_of_distTriang _ (rot_of_distTriang _ hT))) _
        ((rotateRotateRotateIso C).symm.app T)
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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)
H_zero : H 0
H_one : H 1
⊢ H (-1)

Tactic:
have H_neg_one : H (-1) := fun T hT =>
    isomorphic_distinguished _ (inv_rot_of_distTriang _
      (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ hT))) _
        ((invRotateInvRotateInvRotateIso C).symm.app T)
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
⊢ ∀ {a b c : ℤ}, H a → H b → a + b = c → H c

Tactic:
have H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c := fun {a b c} ha hb hc T hT =>
    isomorphic_distinguished _ (hb _ (ha _ hT)) _
      ((Triangle.shiftFunctorAdd' C _ _ _ hc).app T)
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
ofNat : ∀ (n : ℕ), H (Int.ofNat n)
negSucc : ∀ (n : ℕ), H (Int.negSucc n)
⊢ H n

Tactic:
obtain (n | n) := n
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
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)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
⊢ H (Int.ofNat 0)

Tactic:
H_zero

Premises used: Set.Mem, Int.add
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
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)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
⊢ H (Int.ofNat 0)

Tactic:
exact H_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
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)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
hn : H (Int.ofNat n)
⊢ H (Int.ofNat (n + 1))

Tactic:
H_add hn H_one rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
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
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)
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
hn : H (Int.ofNat n)
⊢ H (Int.ofNat (n + 1))

Tactic:
exact H_add hn H_one rfl

Premises used: rfl