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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b = a ≫ T₂.rotate.mor₃
⊢ ∃ (a : T₁.obj₁ ⟶ T₂.obj₁),
    T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
have refine_1 : T₁.mor₁ ≫ b = Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁
Tactic: refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩
-- 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
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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b = a ≫ T₂.rotate.mor₃
refine_1 : T₁.mor₁ ≫ b = Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁
⊢ ∃ (a : T₁.obj₁ ⟶ T₂.obj₁),
    T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
have refine_2 : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.preimage (shiftFunctor C (A := ℤ) 1) a) = c ≫ T₂.mor₃
Tactic: refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩
-- 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
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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b = a ≫ T₂.rotate.mor₃
⊢ T₁.mor₁ ≫ b = Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁
have refine_1 : Eq (α :=
  Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁ ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₂.obj₂)
  (Functor.map (shiftFunctor C (A := ℤ) 1) (T₁.mor₁ ≫ b))
  (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁))
Tactic: apply (shiftFunctor C (1 : ℤ)).map_injective
-- 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ :
  (-Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b =
    a ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₁)
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₂.obj₂)
    (Functor.map (shiftFunctor C (A := ℤ) 1) (T₁.mor₁ ≫ b))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁))
have ha₃ : Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b =
  a ≫ Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₁
Tactic: rw [neg_comp, comp_neg, neg_inj] at ha₂
Cleared hypotheses: ha₂
-- 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
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₂
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ T₁.invRotate.mor₁ ≫ a = Functor.map (shiftFunctor C (A := ℤ) (-1)) c ≫ T₂.invRotate.mor₁
have dsimp : Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
  ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₁.obj₁) ≫
      a :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
  (Functor.map (shiftFunctor C (A := ℤ) (-1)) c ≫
      (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₂.obj₁) :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
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₂
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
have obtain : ∀ (a_1 : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃) (ha₁ : T₁.invRotate.mor₂ ≫ a_1 = a ≫ T₂.invRotate.mor₂)
  (ha₂ :
    T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) =
      a_1 ≫ T₂.invRotate.mor₃),
  ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
Tactic: obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
    (inv_rot_of_distTriang _ hT₁) (inv_rot_of_distTriang _ hT₂) (c⟦(-1 : ℤ)⟧') a (by
    dsimp
    simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
      Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])
-- 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
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₂
a_1 : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a_1 = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a_1 ≫ T₂.invRotate.mor₂
ha₂ :
  T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) =
    a ≫ T₂.invRotate.mor₃
⊢ ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a_1 ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
have refine : T₁.mor₂ ≫ c = a ≫ T₂.mor₂
Tactic: refine ⟨a, ⟨ha₁, ?_⟩⟩
-- 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 : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (X := 0) 0 (𝟙 X) 0)
have refine : Iso (C := Triangle.{v, u} C) (Triangle.mk (X := 0) 0 (𝟙 X) 0) (Triangle.invRotate (contractibleTriangle X))
Tactic: refine isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished X)) _ ?_
-- 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 : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)))
have refine : Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) ≅
  Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)
Tactic: refine isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_
-- 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 : C
⊢ (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X)) =
    Iso.hom (Iso.refl (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).obj₃) ≫
      Triangle.mor₃
        (Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0))
have dsimp : 𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) sorry)) X) =
  𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 sorry)) (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
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
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ ∃ (g : T.obj₃ ⟶ X), f = T.mor₂ ≫ g
have obtain : ∀ (g : T.obj₃ ⟶ obj₃.{v, u} (mk (X := 0) 0 (𝟙 X) 0)) (hg₁ : T.mor₂ ≫ g = f ≫ mor₂ (mk (X := 0) 0 (𝟙 X) 0)),
  T.mor₃ ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) 0 = g ≫ mor₃ (mk (X := 0) 0 (𝟙 X) 0) →
    ∃ (g : T.obj₃ ⟶ X), f = T.mor₂ ≫ g
Tactic: obtain ⟨g, ⟨hg₁, _⟩⟩ := complete_distinguished_triangle_morphism T _ hT
    (contractible_distinguished₁ X) 0 f (by cat_disch)
-- 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
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ ∃ (g : X ⟶ T.obj₁), f = g ≫ T.mor₁
have obtain : ∀ (a : obj₁.{v, u} (contractibleTriangle X) ⟶ T.obj₁) (ha₁ : mor₁ (contractibleTriangle X) ≫ f = a ≫ T.mor₁),
  mor₃ (contractibleTriangle X) ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) a = 0 ≫ T.mor₃ →
    ∃ (g : X ⟶ T.obj₁), f = g ≫ T.mor₁
Tactic: obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ T
    (contractible_distinguished X) hT f 0 (by cat_disch)
-- 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 ↔ Epi T.mor₂
have mp : T.mor₃ = 0 → 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
mp : T.mor₃ = 0 → Epi T.mor₂
⊢ T.mor₃ = 0 ↔ Epi T.mor₂
have mpr : Epi 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
⊢ Epi T.mor₂
have mp : ∀ (R : C) (g : T.obj₃ ⟶ R), T.mor₂ ≫ g = 0 → g = 0
Tactic: rw [epi_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 : T.obj₃ ⟶ X
hg : T.mor₂ ≫ g = 0
⊢ g = 0
have mp : ∀ (f : Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ X) (hg : T.mor₂ ≫ T.mor₃ ≫ f = 0),
  T.mor₃ ≫ f = 0
Tactic: obtain ⟨f, rfl⟩ := yoneda_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 : Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ X
hg : T.mor₂ ≫ T.mor₃ ≫ f = 0
⊢ T.mor₃ ≫ f = 0
have mp : Eq (α := T.obj₃ ⟶ X) (0 ≫ f) 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
X : C
f : Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ X
hg : T.mor₂ ≫ T.mor₃ ≫ f = 0
mp : Eq (α := T.obj₃ ⟶ X) (0 ≫ f) 0
⊢ T.mor₃ ≫ f = 0
have mp₁ : Eq.{v + 1} (α := T.obj₃ ⟶ X) 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 : Epi T.mor₂
⊢ T.mor₃ = 0
have mpr : T.mor₂ ≫ T.mor₃ = T.mor₂ ≫ 0
Tactic: rw [← cancel_epi T.mor₂, comp_distTriang_mor_zero₂₃ _ hT, 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 : Epi T.mor₂
mpr : T.mor₂ ≫ T.mor₃ = T.mor₂ ≫ 0
⊢ T.mor₃ = 0
have mpr₁ : Eq (α := T.obj₂ ⟶ Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) 0 (T.mor₂ ≫ 0)
Tactic: rw [← cancel_epi T.mor₂, comp_distTriang_mor_zero₂₃ _ hT, 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 : Epi T.mor₂
mpr : T.mor₂ ≫ T.mor₃ = T.mor₂ ≫ 0
mpr₁ : Eq (α := T.obj₂ ⟶ Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) 0 (T.mor₂ ≫ 0)
⊢ T.mor₃ = 0
have mpr₂ : Eq.{v + 1} (α := T.obj₂ ⟶ Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₁) 0 0
Tactic: rw [← cancel_epi T.mor₂, comp_distTriang_mor_zero₂₃ _ hT, comp_zero]
-- 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 ↔ Epi T.mor₁
have h : T.invRotate.mor₃ = 0 ↔ Epi T.invRotate.mor₂
Tactic: have h := mor₃_eq_zero_iff_epi₂ _ (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 (α :=
      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₃))
      (T.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.3) 0 ↔
    Epi T.mor₁
⊢ T.mor₂ = 0 ↔ Epi T.mor₁
have rw : T.mor₂ = 0 ↔
  Eq (α :=
    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₃))
    (T.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 sorry)) T.3) 0
Tactic: rw [← h, 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
h :
  Eq (α :=
      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₃))
      (T.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.3) 0 ↔
    Epi T.mor₁
rw :
  T.mor₂ = 0 ↔
    Eq (α :=
      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₃))
      (T.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.3) 0
⊢ T.mor₂ = 0 ↔ Epi T.mor₁
have rw₁ : T.mor₂ = 0 ↔ T.mor₂ = 0
Tactic: rw [← h, IsIso.comp_right_eq_zero]
-- 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 ↔ Epi T.mor₃
have h : T.rotate.mor₃ = 0 ↔ Epi T.rotate.mor₂
Tactic: have h := mor₃_eq_zero_iff_epi₂ _ (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₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.obj₂)
      (-Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.mor₁) 0 ↔
    Epi T.mor₃
⊢ T.mor₁ = 0 ↔ Epi 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) T.obj₂)
    (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) T.mor₁) 0
Tactic: rw [← h, neg_eq_zero]