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
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 n
have have : ∀ (H_zero : H 0), H n
Tactic: have H_zero : H 0 := fun T hT =>
    isomorphic_distinguished _ hT _ ((Triangle.shiftFunctorZero C).app T)
-- 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
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 n
have H_one : 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)
-- 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
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 n
have H_neg_one : 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)
-- 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
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 n
have H_add : ∀ {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)
-- 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)
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 n
have ofNat : ∀ (n : ℕ), H (Int.ofNat n)
Tactic: obtain (n | n) := n
Cleared hypotheses: n
-- 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)
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)
⊢ H n
have negSucc : ∀ (n : ℕ), H (Int.negSucc n)
Tactic: obtain (n | n) := n
Cleared hypotheses: n
-- 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
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 : ℕ
⊢ H (Int.ofNat n)
have ofNat : H (Int.ofNat 0)
Tactic: induction n with
    | zero => exact H_zero
    | succ n hn => exact H_add hn H_one rfl
Cleared hypotheses: n
-- 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
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 : ℕ
ofNat : H (Int.ofNat 0)
⊢ H (Int.ofNat n)
have ofNat₁ : ∀ (n : ℕ) (hn : H (Int.ofNat n)), H (Int.ofNat (n + 1))
Tactic: induction n with
    | zero => exact H_zero
    | succ n hn => exact H_add hn H_one rfl
Cleared hypotheses: n
-- 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
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 : ℕ
⊢ H (Int.negSucc n)
have negSucc : H (Int.negSucc 0)
Tactic: induction n with
    | zero => exact H_neg_one
    | succ n hn => exact H_add hn H_neg_one rfl
Cleared hypotheses: n
-- 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
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 : ℕ
negSucc : H (Int.negSucc 0)
⊢ H (Int.negSucc n)
have negSucc₁ : ∀ (n : ℕ) (hn : H (Int.negSucc n)), H (Int.negSucc (n + 1))
Tactic: induction n with
    | zero => exact H_neg_one
    | succ n hn => exact H_add hn H_neg_one rfl
Cleared hypotheses: n
-- 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
h : IsZero.{v, u} T.obj₁
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T ↔ IsIso T.mor₂
have rw : IsIso T.rotate.mor₁ ↔ IsIso T.mor₂
Tactic: rw [rotate_distinguished_triangle,
    distinguished_iff_of_isZero₃ _ (Functor.map_isZero (CategoryTheory.shiftFunctor C 1) 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
h : IsZero.{v, u} T.obj₂
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T ↔ IsIso T.mor₃
have rw : IsIso T.rotate.mor₂ ↔ IsIso T.mor₃
Tactic: rw [rotate_distinguished_triangle, distinguished_iff_of_isZero₁ _ 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
⊢ IsSplitEpi f
have obtain : ∀ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
  (hT :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)),
  IsSplitEpi f
Tactic: obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
⊢ 𝟙 (Triangle.mk f g h).obj₂ ≫ (Triangle.mk f g h).mor₂ = 0
have rw : Eq.{v + 1} (α := (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₃) (𝟙 (Triangle.mk f g h).obj₂ ≫ 0) 0
Tactic: rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
rw : Eq.{v + 1} (α := (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₃) (𝟙 (Triangle.mk f g h).obj₂ ≫ 0) 0
⊢ 𝟙 (Triangle.mk f g h).obj₂ ≫ (Triangle.mk f g h).mor₂ = 0
have rw₁ : Eq.{v + 1} (α := (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₃) 0 0
Tactic: rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
Z : C
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
⊢ IsSplitEpi f
have obtain : ∀ (r : (Triangle.mk f g h).obj₂ ⟶ (Triangle.mk f g h).obj₁)
  (hr : 𝟙 (Triangle.mk f g h).obj₂ = r ≫ (Triangle.mk f g h).mor₁), IsSplitEpi f
Tactic: obtain ⟨r, hr⟩ := Triangle.coyoneda_exact₂ _ hT (𝟙 _)
      (by rw [Triangle.mor₂_eq_zero_of_epi₁ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X Y : C
f : X ⟶ Y
hf : Mono f
⊢ IsSplitMono f
have obtain : ∀ (X_1 : C) (g : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X_1)
  (hT :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk g f h)),
  IsSplitMono f
Tactic: obtain ⟨X, g, h, hT⟩ := distinguished_cocone_triangle₁ f
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
⊢ (Triangle.mk g f h).mor₁ ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0
have rw : Eq.{v + 1} (α := (Triangle.mk g f h).obj₁ ⟶ (Triangle.mk g f h).obj₂) (0 ≫ 𝟙 (Triangle.mk g f h).obj₂) 0
Tactic: rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
rw : Eq.{v + 1} (α := (Triangle.mk g f h).obj₁ ⟶ (Triangle.mk g f h).obj₂) (0 ≫ 𝟙 (Triangle.mk g f h).obj₂) 0
⊢ (Triangle.mk g f h).mor₁ ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0
have rw₁ : Eq.{v + 1} (α := (Triangle.mk g f h).obj₁ ⟶ (Triangle.mk g f h).obj₂) 0 0
Tactic: rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
X_1 Y : C
f : X_1 ⟶ Y
hf : Mono f
X : C
g : X ⟶ X_1
h : Y ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f h)
⊢ IsSplitMono f
have obtain : ∀ (r : (Triangle.mk g f h).obj₃ ⟶ (Triangle.mk g f h).obj₂)
  (hr : 𝟙 (Triangle.mk g f h).obj₂ = (Triangle.mk g f h).mor₂ ≫ r), IsSplitMono f
Tactic: obtain ⟨r, hr⟩ := Triangle.yoneda_exact₂ _ hT (𝟙 _) (by
      rw [Triangle.mor₁_eq_zero_of_mono₂ _ hT hf, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
⊢ Mono φ.hom₂
have rw : ∀ (P : C) (g : P ⟶ T.obj₂), g ≫ φ.hom₂ = 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
⊢ f ≫ T.mor₂ = 0
have rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
Tactic: rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
⊢ f ≫ T.mor₂ = 0
have rw₁ : f ≫ T.mor₂ ≫ φ.hom₃ = 0 ≫ φ.hom₃
Tactic: rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₁ : f ≫ T.mor₂ ≫ φ.hom₃ = 0 ≫ φ.hom₃
⊢ f ≫ T.mor₂ = 0
have rw₂ : f ≫ φ.hom₂ ≫ T'.mor₂ = 0 ≫ φ.hom₃
Tactic: rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₁ : f ≫ T.mor₂ ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₂ : f ≫ φ.hom₂ ≫ T'.mor₂ = 0 ≫ φ.hom₃
⊢ f ≫ T.mor₂ = 0
have rw₃ : Eq (α := A ⟶ T'.obj₃) (0 ≫ T'.mor₂) (0 ≫ φ.hom₃)
Tactic: rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₁ : f ≫ T.mor₂ ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₂ : f ≫ φ.hom₂ ≫ T'.mor₂ = 0 ≫ φ.hom₃
rw₃ : Eq (α := A ⟶ T'.obj₃) (0 ≫ T'.mor₂) (0 ≫ φ.hom₃)
⊢ f ≫ T.mor₂ = 0
have rw₄ : Eq (α := A ⟶ T'.obj₃) 0 (0 ≫ φ.hom₃)
Tactic: rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
rw : (f ≫ T.mor₂) ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₁ : f ≫ T.mor₂ ≫ φ.hom₃ = 0 ≫ φ.hom₃
rw₂ : f ≫ φ.hom₂ ≫ T'.mor₂ = 0 ≫ φ.hom₃
rw₃ : Eq (α := A ⟶ T'.obj₃) (0 ≫ T'.mor₂) (0 ≫ φ.hom₃)
rw₄ : Eq (α := A ⟶ T'.obj₃) 0 (0 ≫ φ.hom₃)
⊢ f ≫ T.mor₂ = 0
have rw₅ : Eq.{v + 1} (α := A ⟶ T'.obj₃) 0 0
Tactic: rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
f : A ⟶ T.obj₂
hf : f ≫ φ.hom₂ = 0
⊢ f = 0
have obtain : ∀ (g : A ⟶ T.obj₁) (hf : (g ≫ T.mor₁) ≫ φ.hom₂ = 0), g ≫ T.mor₁ = 0
Tactic: obtain ⟨g, rfl⟩ := Triangle.coyoneda_exact₂ _ hT f
      (by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp])
Cleared hypotheses: f, hf