awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Iso (C := Triangle.{v_2, u_2} D) (obj F.mapTriangle T) (obj F.mapTriangle (Triangle.mk T.mor₁ g h))

Tactic:
exact isoTriangleOfIso₁₂ _ _ hT (F.map_distinguished _ mem)
    (Iso.refl _) (Iso.refl _) (by simp)

Premises used: CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂, CategoryTheory.Iso.refl, 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 ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
mp : F₁.IsTriangulated → F₂.IsTriangulated
mpr : F₂.IsTriangulated → F₁.IsTriangulated
⊢ F₁.IsTriangulated ↔ F₂.IsTriangulated

Tactic:
constructor
-- 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 ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
h : F₁.IsTriangulated
⊢ F₂.IsTriangulated

Tactic:
isTriangulated_of_iso e

Premises used: CategoryTheory.Functor.isTriangulated_of_iso
-- 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 ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
h : F₁.IsTriangulated
⊢ F₂.IsTriangulated

Tactic:
exact isTriangulated_of_iso e

Premises used: CategoryTheory.Functor.isTriangulated_of_iso
-- 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 ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
h : F₂.IsTriangulated
⊢ NatTrans.CommShift e.symm.hom ℤ

Tactic:
have : NatTrans.CommShift e.symm.hom ℤ := inferInstanceAs (NatTrans.CommShift e.inv ℤ)
-- 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 ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
h : F₂.IsTriangulated
this : NatTrans.CommShift e.symm.hom ℤ
⊢ F₁.IsTriangulated

Tactic:
isTriangulated_of_iso e.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.isTriangulated_of_iso
-- 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 ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
h : F₂.IsTriangulated
this : NatTrans.CommShift e.symm.hom ℤ
⊢ F₁.IsTriangulated

Tactic:
exact isTriangulated_of_iso e.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.isTriangulated_of_iso
-- 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 ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
rw : F.IsTriangulated ↔ (F ⋙ G).IsTriangulated
⊢ F.IsTriangulated ↔ H.IsTriangulated

Tactic:
rw [← isTriangulated_iff_of_iso e]

Premises used: CategoryTheory.Functor.isTriangulated_iff_of_iso
-- 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 ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
⊢ F.IsTriangulated ↔ (F ⋙ G).IsTriangulated

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun T hT ↦ ?_⟩⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Functor.IsTriangulated.mk
-- 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 ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
refine :
  (F ⋙ G).IsTriangulated →
    ∀ (T : Triangle.{v_1, u_1} C)
      (hT :
        Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_6 _ inst_9 inst_12 _) T),
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_7 _ inst_10 inst_13 _)
        (obj F.mapTriangle T)
⊢ F.IsTriangulated ↔ (F ⋙ G).IsTriangulated

Tactic:
refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun T hT ↦ ?_⟩⟩
-- 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 ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
h : (F ⋙ G).IsTriangulated
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_6 _ inst_9 inst_12 _) T
rw :
  Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _)
    (obj (C := Triangle.{v_2, u_2} D) G.mapTriangle (obj F.mapTriangle T))
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_7 _ inst_10 inst_13 _)
    (obj F.mapTriangle T)

Tactic:
rw [← G.map_distinguished_iff]

Premises used: CategoryTheory.Functor.map_distinguished_iff
-- 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 ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
h : (F ⋙ G).IsTriangulated
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_6 _ inst_9 inst_12 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _)
    (obj (C := Triangle.{v_2, u_2} D) G.mapTriangle (obj F.mapTriangle T))

Tactic:
isomorphic_distinguished _ ((F ⋙ G).map_distinguished T hT) _
    ((mapTriangleCompIso F G).symm.app T)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, CategoryTheory.Iso.app, 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 ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
h : (F ⋙ G).IsTriangulated
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_6 _ inst_9 inst_12 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _)
    (obj (C := Triangle.{v_2, u_2} D) G.mapTriangle (obj F.mapTriangle T))

Tactic:
exact isomorphic_distinguished _ ((F ⋙ G).map_distinguished T hT) _
    ((mapTriangleCompIso F G).symm.app T)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, CategoryTheory.Iso.app, 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.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _) T
e : F.mapArrow.obj (F.mapArrow.objPreimage (Arrow.mk T.mor₁)) ≅ Arrow.mk T.mor₁ :=
  F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
⊢ ∃ (X : C) (Y : C) (f : X ⟶ Y) (e₁ : F.obj X ≅ T.obj₁) (e₂ : F.obj Y ≅ T.obj₂), F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁

Tactic:
⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩

Premises used: CategoryTheory.Arrow.Hom.w, CategoryTheory.Arrow.leftFunc, Exists.intro, CategoryTheory.Arrow.rightFunc, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.mapIso
-- 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.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _) T
e : F.mapArrow.obj (F.mapArrow.objPreimage (Arrow.mk T.mor₁)) ≅ Arrow.mk T.mor₁ :=
  F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
⊢ ∃ (X : C) (Y : C) (f : X ⟶ Y) (e₁ : F.obj X ≅ T.obj₁) (e₂ : F.obj Y ≅ T.obj₂), F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁

Tactic:
exact ⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩
-- 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.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _) T
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
obtain :
  ∀ (W : C) (g : Y ⟶ W) (h : W ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (H :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
        (Triangle.mk f g h)),
    ∃ (T' : Triangle.{v_1, u_1} C) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T'),
      Nonempty.{v_2 + 1} (obj F.mapTriangle T' ≅ T)
⊢ ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T'),
    Nonempty.{v_2 + 1} (obj F.mapTriangle T' ≅ T)

Tactic:
obtain ⟨W, g, h, H⟩ := distinguished_cocone_triangle f

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- 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.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _) T
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
W : C
g : Y ⟶ W
h : W ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk f g h)
⊢ ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T'),
    Nonempty.{v_2 + 1} (obj F.mapTriangle T' ≅ T)

Tactic:
⟨_, H, ⟨isoTriangleOfIso₁₂ _ _ (F.map_distinguished _ H) hT e₁ e₂ w⟩⟩

Premises used: CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂, Nonempty.intro, Exists.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.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _) T
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
W : C
g : Y ⟶ W
h : W ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk f g h)
⊢ ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T'),
    Nonempty.{v_2 + 1} (obj F.mapTriangle T' ≅ T)

Tactic:
exact ⟨_, H, ⟨isoTriangleOfIso₁₂ _ _ (F.map_distinguished _ H) hT e₁ e₂ w⟩⟩