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 ℤ
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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
⊢ ∃ (α : ComposableArrows.{v_1, u_1} C 2),
    Nonempty.{v_2 + 1} (Functor.obj (F.mapComposableArrows 2) α ≅ ComposableArrows.mk₂ u₁₂ u₂₃)

Tactic:
⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
octahedron_axiom :
  ∀ (α : ComposableArrows.{v_1, u_1} C 2) (e : Functor.obj (F.mapComposableArrows 2) α ≅ ComposableArrows.mk₂ u₁₂ u₂₃),
    Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
obtain ⟨α, ⟨e⟩⟩ : ∃ (α : ComposableArrows C 2),
      Nonempty ((F.mapComposableArrows 2).obj α ≅ ComposableArrows.mk₂ u₁₂ u₂₃) :=
    ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Premises used: CategoryTheory.ComposableArrows, OfNat.ofNat
-- 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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
α : ComposableArrows.{v_1, u_1} C 2
e : Functor.obj (F.mapComposableArrows 2) α ≅ ComposableArrows.mk₂ u₁₂ u₂₃
octahedron_axiom :
  ∀ (X₁ X₂ X₃ : C) (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
    (e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃),
    Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
obtain ⟨X₁, X₂, X₃, f, g, rfl⟩ := ComposableArrows.mk₂_surjective α

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective
-- 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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
octahedron_axiom :
  ∀ (w : C) (w_1 : X₂ ⟶ w) (w_2 : w ⟶ 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 f w_1 w_2)),
    Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
obtain ⟨_, _, _, 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 ℤ
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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
w : C
w_1 : X₂ ⟶ w
w_2 : w ⟶ 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 f w_1 w_2)
octahedron_axiom :
  ∀ (w : C) (w_3 : X₃ ⟶ w) (w_4 : w ⟶ 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 g w_3 w_4)),
    Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
obtain ⟨_, _, _, h₂₃'⟩ := distinguished_cocone_triangle g

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 ℤ
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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
w : C
w_1 : X₂ ⟶ w
w_2 : w ⟶ 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 f w_1 w_2)
w_3 : C
w_4 : X₃ ⟶ w_3
w_5 : w_3 ⟶ 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 g w_4 w_5)
octahedron_axiom :
  ∀ (w : C) (w_6 : X₃ ⟶ w) (w_7 : w ⟶ 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 (f ≫ g) w_6 w_7)),
    Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
obtain ⟨_, _, _, h₁₃'⟩ := distinguished_cocone_triangle (f ≫ g)

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.CategoryStruct.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
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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
w : C
w_1 : X₂ ⟶ w
w_2 : w ⟶ 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 f w_1 w_2)
w_3 : C
w_4 : X₃ ⟶ w_3
w_5 : w_3 ⟶ 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 g w_4 w_5)
w_6 : C
w_7 : X₃ ⟶ w_6
w_8 : w_6 ⟶ 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 (f ≫ g) w_7 w_8)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
⟨Octahedron.ofIso (e₁ := (e.app 0).symm) (e₂ := (e.app 1).symm) (e₃ := (e.app 2).symm)
    (comm₁₂ := ComposableArrows.naturality' e.inv 0 1)
    (comm₂₃ := ComposableArrows.naturality' e.inv 1 2)
    (H := (someOctahedron rfl h₁₂' h₂₃' h₁₃').map F) ..⟩

Premises used: CategoryTheory.Triangulated.Octahedron.ofIso, CategoryTheory.Triangulated.someOctahedron, CategoryTheory.Triangulated.Octahedron.map, Nonempty.intro, CategoryTheory.ComposableArrows.naturality', CategoryTheory.Iso.symm, CategoryTheory.Iso.app, OfNat.ofNat, CategoryTheory.Iso.inv, rfl
-- 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
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
w : C
w_1 : X₂ ⟶ w
w_2 : w ⟶ 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 f w_1 w_2)
w_3 : C
w_4 : X₃ ⟶ w_3
w_5 : w_3 ⟶ 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 g w_4 w_5)
w_6 : C
w_7 : X₃ ⟶ w_6
w_8 : w_6 ⟶ 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 (f ≫ g) w_7 w_8)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
exact ⟨Octahedron.ofIso (e₁ := (e.app 0).symm) (e₂ := (e.app 1).symm) (e₃ := (e.app 2).symm)
    (comm₁₂ := ComposableArrows.naturality' e.inv 0 1)
    (comm₂₃ := ComposableArrows.naturality' e.inv 1 2)
    (H := (someOctahedron rfl h₁₂' h₂₃' h₁₃').map F) ..⟩
-- 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 : F.Full
inst_15 : F.Faithful
inst_16 : IsTriangulated.{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₁₃)
rw : F.map u₁₂ ≫ F.map u₂₃ = F.map (u₁₂ ≫ u₂₃)
rw₁ rw₂ : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₂ ≫ F.map u₂₃
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃

Tactic:
rw [← comm, F.map_comp]

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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : F.Full
inst_15 : F.Faithful
inst_16 : IsTriangulated.{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₁₃)
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃

Tactic:
have comm' : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃ := by rw [← comm, F.map_comp]