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 ⋙ G).IsTriangulated
inst_21 : F.IsTriangulated
inst_22 : F.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_12 inst_15 _) T
obtain :
  ∀ (T' : Triangle.{v_1, u_1} C)
    (hT' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _) T')
    (e : obj F.mapTriangle T' ≅ T),
    Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_10 _ inst_13 inst_16 _)
      (obj G.mapTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_10 _ inst_13 inst_16 _)
    (obj G.mapTriangle T)

Tactic:
obtain ⟨T', hT', ⟨e⟩⟩ := F.mem_mapTriangle_essImage_of_distinguished T hT

Premises used: CategoryTheory.Functor.mem_mapTriangle_essImage_of_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 ⋙ G).IsTriangulated
inst_21 : F.IsTriangulated
inst_22 : F.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_12 inst_15 _) T
T' : Triangle.{v_1, u_1} C
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _) T'
e : obj F.mapTriangle T' ≅ T
⊢ Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_10 _ inst_13 inst_16 _)
    (obj G.mapTriangle T)

Tactic:
isomorphic_distinguished _ ((F ⋙ G).map_distinguished T' hT') _
      (G.mapTriangle.mapIso e.symm ≪≫ (mapTriangleCompIso F G).symm.app _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, 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 ⋙ G).IsTriangulated
inst_21 : F.IsTriangulated
inst_22 : F.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_12 inst_15 _) T
T' : Triangle.{v_1, u_1} C
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _) T'
e : obj F.mapTriangle T' ≅ T
⊢ Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_10 _ inst_13 inst_16 _)
    (obj G.mapTriangle T)

Tactic:
exact isomorphic_distinguished _ ((F ⋙ G).map_distinguished T' hT') _
      (G.mapTriangle.mapIso e.symm ≪≫ (mapTriangleCompIso F G).symm.app _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, 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
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_20 : H.CommShift ℤ
inst_21 : H.IsTriangulated
inst_22 : F.IsTriangulated
inst_23 : F.mapArrow.EssSurj
inst_24 : NatTrans.CommShift e.hom ℤ
⊢ (F ⋙ G).IsTriangulated

Tactic:
have := (isTriangulated_iff_of_iso e).2 inferInstance
-- 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
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_20 : H.CommShift ℤ
inst_21 : H.IsTriangulated
inst_22 : F.IsTriangulated
inst_23 : F.mapArrow.EssSurj
inst_24 : NatTrans.CommShift e.hom ℤ
this : (F ⋙ G).IsTriangulated
⊢ G.IsTriangulated

Tactic:
isTriangulated_of_precomp F G

Premises used: CategoryTheory.Functor.isTriangulated_of_precomp
-- 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
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_20 : H.CommShift ℤ
inst_21 : H.IsTriangulated
inst_22 : F.IsTriangulated
inst_23 : F.mapArrow.EssSurj
inst_24 : NatTrans.CommShift e.hom ℤ
this : (F ⋙ G).IsTriangulated
⊢ G.IsTriangulated

Tactic:
exact isTriangulated_of_precomp F G

Premises used: CategoryTheory.Functor.isTriangulated_of_precomp
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
dsimp : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
⊢ F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁ ≫ F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁ = F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁

Tactic:
dsimp
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
rw : F.map (u₁₂ ≫ u₂₃) = F.map u₁₃
rw₁ rw₂ : F.map u₁₃ = F.map u₁₃
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃

Tactic:
rw [← F.map_comp, comm]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
⊢ F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₂ ≫ F.map h.m₁ =
    F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁ ≫ F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂

Tactic:
simpa using F.congr_map h.comm₁

Premises used: CategoryTheory.Triangulated.Octahedron.comm₁, CategoryTheory.Functor.congr_map
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
⊢ Eq (α :=
    F.obj (Triangle.mk u₁₂ v₁₂ w₁₂).obj₃ ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F.obj (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
    (F.map h.m₁ ≫
      F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁)
    (F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁)

Tactic:
simpa using F.congr_map h.comm₂ =≫ (F.commShiftIso 1).hom.app X₁

Premises used: CategoryTheory.Triangulated.Octahedron.comm₂, CategoryTheory.Functor.congr_map, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
⊢ F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂ ≫ F.map h.m₃ = F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₂

Tactic:
simpa using F.congr_map h.comm₃

Premises used: CategoryTheory.Functor.congr_map, CategoryTheory.Triangulated.Octahedron.comm₃
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.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_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
⊢ Eq (α :=
    F.obj (Triangle.mk u₁₃ v₁₃ w₁₃).obj₃ ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F.obj (Triangle.mk u₁₂ v₁₂ w₁₂).obj₂))
    ((F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁))
    (F.map h.m₃ ≫
      F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁)

Tactic:
simpa using F.congr_map h.comm₄ =≫ (F.commShiftIso 1).hom.app X₂

Premises used: CategoryTheory.Functor.congr_map, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.Triangulated.Octahedron.comm₄, CategoryTheory.NatTrans.app
-- 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 : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.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 : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
octahedron_axiom :
  ∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : D} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂}
    {w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X₁}
    (h₁₂ :
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
        (Triangle.mk u₁₂ v₁₂ w₁₂))
    {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X₂}
    (h₂₃ :
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
        (Triangle.mk u₂₃ v₂₃ w₂₃))
    {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X₁}
    (h₁₃ :
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
        (Triangle.mk u₁₃ v₁₃ w₁₃)),
    Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
⊢ IsTriangulated.{v_2, u_2} D

Tactic:
apply IsTriangulated.mk

Premises used: CategoryTheory.IsTriangulated.mk