awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
h₁ :
  CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
        (prodComparison F X₁ X₃))
      prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃)) (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
      prod.fst
h₂ :
  CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
        (prodComparison F X₁ X₃))
      prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃)) (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
      prod.snd
⊢ Eq (α := F.obj X₁ ⟶ Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
      (prodComparison F X₁ X₃))
    (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
⊢ CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
        (prodComparison F X₁ X₃))
      prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃)) (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
      prod.snd

Tactic:
simp only [assoc, prodComparison_snd, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_right, BinaryFan.mk_snd,
            ← F.map_comp, F.map_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Category.comp_id, CategoryTheory.Limits.BinaryFan.π_app_right, CategoryTheory.Limits.BinaryFan.mk_snd, CategoryTheory.Limits.prodComparison_snd, CategoryTheory.Limits.prod.comp_lift, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.BinaryFan.mk_pt
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
⊢ Triangle.mor₂ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃)) ≫
      𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))) =
    CategoryStruct.comp (Y := Triangle.obj₂.{v_2, u_2} (binaryProductTriangle (F.obj X₁) (F.obj X₃)))
      (prodComparison F X₁ X₃) (Triangle.mor₂ (binaryProductTriangle (F.obj X₁) (F.obj X₃)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
⊢ Triangle.mor₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃)) ≫
      map (shiftFunctor D (A := ℤ) 1)
        (𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃)))) =
    𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))) ≫
      Triangle.mor₃ (binaryProductTriangle (F.obj X₁) (F.obj X₃))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
dsimp : IsIso.{v_2, u_2} (𝟙 (F.obj X₁))
⊢ IsIso φ.hom₁

Tactic:
dsimp [φ]
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso.{v_2, u_2} (𝟙 (F.obj X₁))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
dsimp : IsIso.{v_2, u_2} (𝟙 (F.obj X₃))
⊢ IsIso φ.hom₃

Tactic:
dsimp [φ]
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso.{v_2, u_2} (𝟙 (F.obj X₃))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (prodComparison F X₁ X₃)

Tactic:
exact isIso₂_of_isIso₁₃ φ (F.map_distinguished _ (binaryProductTriangle_distinguished X₁ X₃))
    (binaryProductTriangle_distinguished _ _)
    (by dsimp [φ]; infer_instance) (by dsimp [φ]; infer_instance)

Premises used: CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃, CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
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 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
⊢ F.Additive

Tactic:
F.additive_of_preserves_binary_products

Premises used: CategoryTheory.Functor.additive_of_preserves_binary_products
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
      (obj F.mapTriangle T) ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T

Tactic:
⟨fun hT ↦ ?_, F.map_distinguished T⟩

Premises used: Iff.intro, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
refine :
  ∀
    (hT :
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
        (obj F.mapTriangle T)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
      (obj F.mapTriangle T) ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T

Tactic:
refine ⟨fun hT ↦ ?_, F.map_distinguished T⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)
obtain :
  ∀ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)
    (mem :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
        (Triangle.mk T.mor₁ g h)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T

Tactic:
obtain ⟨Z, g, h, mem⟩ := distinguished_cocone_triangle T.mor₁

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.Pretriangulated.Triangle.mor₁
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk T.mor₁ g h)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T

Tactic:
isomorphic_distinguished _ mem _ (F.mapTriangle.preimageIso ?_)

Premises used: CategoryTheory.Functor.mapTriangle, CategoryTheory.Functor.preimageIso, CategoryTheory.Pretriangulated.isomorphic_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk T.mor₁ g h)
refine : Iso (C := Triangle.{v_2, u_2} D) (obj F.mapTriangle T) (obj F.mapTriangle (Triangle.mk T.mor₁ g h))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T

Tactic:
refine isomorphic_distinguished _ mem _ (F.mapTriangle.preimageIso ?_)

Premises used: CategoryTheory.Functor.mapTriangle, CategoryTheory.Functor.preimageIso, CategoryTheory.Pretriangulated.isomorphic_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk T.mor₁ g h)
⊢ Triangle.mor₁ (obj F.mapTriangle T) ≫ Iso.hom (Iso.refl (Triangle.obj₂ (obj F.mapTriangle T))) =
    Iso.hom (Iso.refl (Triangle.obj₁ (obj F.mapTriangle T))) ≫
      Triangle.mor₁ (obj F.mapTriangle (Triangle.mk T.mor₁ g h))

Tactic:
simp