awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
h₁ : m.hom₁ = TriangleMorphism.hom₁ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
h₂ : m.hom₂ = TriangleMorphism.hom₂ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
⊢ m = (fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s
have h₃ : m.hom₃ = TriangleMorphism.hom₃ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
⊢ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (productTriangle T).mor₁ = 0
have this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
Tactic: have : HasProduct (fun j => (T j).obj₂⟦(1 : ℤ)⟧) :=
    ⟨_, isLimitFanMkObjOfIsLimit (shiftFunctor C (1 : ℤ)) _ _
      (productIsProduct (fun j => (T j).obj₂))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
⊢ (productTriangle T).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (productTriangle T).mor₁ = 0
have dsimp : Eq.{v + 1} (α :=
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
  (CategoryStruct.comp (Y :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
    (CategoryStruct.comp (Y :=
      piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
      (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Limits.Pi.map fun (j : J) ↦ (T j).mor₁)))
  0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
⊢ Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Limits.Pi.map fun (j : J) ↦ (T j).mor₁)))
    0
have change : Eq.{v + 1} (α :=
  (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
  (CategoryStruct.comp (Y :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
    (CategoryStruct.comp (Y :=
      piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
      (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁)))
  0
Tactic: change _ ≫ (Pi.lift (fun j => Pi.π _ j ≫ (T j).mor₁))⟦(1 : ℤ)⟧' = 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
⊢ Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁)))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁)))
    0
have rw : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃)
    (piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂))
  (CategoryStruct.comp (Y :=
    piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
    (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
      (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁))
        (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₂))))
  0
Tactic: rw [assoc, ← cancel_mono (piComparison _ _), zero_comp, assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x_1) (B.obj x_1) } =
    { hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ
have h₁ : (A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := sorry, comm₂ := sorry, comm₃ := sorry :
        TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₁ =
  TriangleMorphism.hom₁
    ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := sorry, comm₂ := sorry, comm₃ := sorry :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
h₁ :
  (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₁ =
    TriangleMorphism.hom₁
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)
⊢ A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x_1) (B.obj x_1) } =
    { hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ
have h₂ : (A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := sorry, comm₂ := sorry, comm₃ := sorry :
        TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₂ =
  TriangleMorphism.hom₂
    ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := sorry, comm₂ := sorry, comm₃ := sorry :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
h₁ :
  (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₁ =
    TriangleMorphism.hom₁
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)
h₂ :
  (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₂ =
    TriangleMorphism.hom₂
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)
⊢ A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x_1) (B.obj x_1) } =
    { hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ
have h₃ : (A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := sorry, comm₂ := sorry, comm₃ := sorry :
        TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₃ =
  TriangleMorphism.hom₃
    ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := sorry, comm₂ := sorry, comm₃ := sorry :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C (A := ℤ) 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.inv (shiftFunctor C (A := ℤ) 1) = iso₃.inv ≫ A.whiskerLeft π₃Toπ₁
have simp : A.whiskerLeft π₃Toπ₁ ≫ 𝟙 ((A ⋙ π₁) ⋙ shiftFunctor C (A := ℤ) 1) = A.whiskerLeft π₃Toπ₁
Tactic: simp only [← cancel_epi iso₃.hom, ← reassoc_of% comm₃, Iso.hom_inv_id_assoc,
        ← whiskerRight_comp, Iso.hom_inv_id, whiskerRight_id']
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α :=
    Triangle.obj₁
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ⟶
      Triangle.obj₂
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
    (Triangle.mor₁
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ≫
      F.map f.hom₂)
    (F.map f.hom₁ ≫
      Triangle.mor₁
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
have dsimp : F.map X.mor₁ ≫ F.map f.hom₂ = F.map f.hom₁ ≫ F.map Y.mor₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α :=
    Triangle.obj₂
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ⟶
      Triangle.obj₃
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
    (Triangle.mor₂
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ≫
      F.map f.hom₃)
    (F.map f.hom₂ ≫
      Triangle.mor₂
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
have dsimp : F.map X.mor₂ ≫ F.map f.hom₃ = F.map f.hom₂ ≫ F.map Y.mor₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α :=
    Triangle.obj₃
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
        (Triangle.obj₁
          (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂)
            (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁))))
    (Triangle.mor₃
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map f.hom₁))
    (F.map f.hom₃ ≫
      Triangle.mor₃
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
have dsimp : Eq (α := F.obj X.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F.obj Y.obj₁))
  ((F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁) ≫ map (shiftFunctor D (A := ℤ) 1) (F.map f.hom₁))
  (F.map f.hom₃ ≫ F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
Tactic: dsimp [Functor.comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ f = g
have h₁ : f.hom₁ = g.hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
h₁ : f.hom₁ = g.hom₁
⊢ f = g
have h₂ : f.hom₂ = g.hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
h₁ : f.hom₁ = g.hom₁
h₂ : f.hom₂ = g.hom₂
⊢ f = g
have h₃ : f.hom₃ = g.hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ f.hom₁ = g.hom₁
have h₁ : F.map f.hom₁ = F.map g.hom₁
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ f.hom₂ = g.hom₂
have h₂ : F.map f.hom₂ = F.map g.hom₂
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ f.hom₃ = g.hom₃
have h₃ : F.map f.hom₃ = F.map g.hom₃
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Full
inst_9 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)
⊢ F.map (X.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) (F.preimage f.hom₁)) = F.map (F.preimage f.hom₃ ≫ Y.mor₃)
have rw : Eq (α := F.obj X.obj₃ ⟶ (F ⋙ shiftFunctor D (A := ℤ) 1).obj Y.obj₁)
  (F.map (X.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) (F.preimage f.hom₁)) ≫
    NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
  (F.map (F.preimage f.hom₃ ≫ Y.mor₃) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
Tactic: rw [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app Y.obj₁)]