awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
h : a + b = c
subst :
  Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) (a + b))
      (CategoryTheory.shiftFunctor (Triangle.{v, u} C) a ⋙ CategoryTheory.shiftFunctor (Triangle.{v, u} C) b))
    (CategoryTheory.shiftFunctorAdd' (Triangle.{v, u} C) a b (a + b) ⋯) (shiftFunctorAdd' C a b (a + b) ⋯)
⊢ Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) c)
      (CategoryTheory.shiftFunctor (Triangle.{v, u} C) a ⋙ CategoryTheory.shiftFunctor (Triangle.{v, u} C) b))
    (CategoryTheory.shiftFunctorAdd' (Triangle.{v, u} C) a b c h) (shiftFunctorAdd' C a b c h)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
rw :
  Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) (a + b))
      (CategoryTheory.shiftFunctor (Triangle.{v, u} C) a ⋙ CategoryTheory.shiftFunctor (Triangle.{v, u} C) b))
    (shiftFunctorAdd (Triangle.{v, u} C) a b) (shiftFunctorAdd' C a b (a + b) ⋯)
⊢ Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) (a + b))
      (CategoryTheory.shiftFunctor (Triangle.{v, u} C) a ⋙ CategoryTheory.shiftFunctor (Triangle.{v, u} C) b))
    (CategoryTheory.shiftFunctorAdd' (Triangle.{v, u} C) a b (a + b) ⋯) (shiftFunctorAdd' C a b (a + b) ⋯)

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd]

Premises used: CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Triangulated.TriangleShift
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
⊢ Eq (α :=
    Iso (C := Triangle.{v, u} C ⥤ Triangle.{v, u} C) (CategoryTheory.shiftFunctor (Triangle.{v, u} C) (a + b))
      (CategoryTheory.shiftFunctor (Triangle.{v, u} C) a ⋙ CategoryTheory.shiftFunctor (Triangle.{v, u} C) b))
    (shiftFunctorAdd (Triangle.{v, u} C) a b) (shiftFunctorAdd' C a b (a + b) ⋯)

Tactic:
apply shiftFunctorAdd_eq

Premises used: CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd_eq
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Triangle.obj₁.{v_1, u_1}
      (Triangle.mk (X := 0) (Y := 0) (Z := 0) 0 0
        (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) 0
          (Functor.map (shiftFunctor C (A := ℤ) 1) 0))) ≅
    Triangle.obj₁.{v_1, u_1}
      (Triangle.mk (X := 0) (Y := 0) (Z := 0) 0 0
        (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) 0
          (Functor.map (shiftFunctor C (A := ℤ) 1) 0)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Triangle.obj₂.{v_1, u_1}
      (Triangle.mk (X := 0) (Y := 0) (Z := 0) 0 0
        (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) 0
          (Functor.map (shiftFunctor C (A := ℤ) 1) 0))) ≅
    Triangle.obj₂.{v_1, u_1}
      (Triangle.mk (X := 0) (Y := 0) (Z := 0) 0 0
        (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) 0
          (Functor.map (shiftFunctor C (A := ℤ) 1) 0)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Triangle.obj₃.{v_1, u_1}
      (Triangle.mk (X := 0) (Y := 0) (Z := 0) 0 0
        (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) 0
          (Functor.map (shiftFunctor C (A := ℤ) 1) 0))) ≅
    Triangle.obj₃.{v_1, u_1}
      (Triangle.mk (X := 0) (Y := 0) (Z := 0) 0 0
        (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) 0
          (Functor.map (shiftFunctor C (A := ℤ) 1) 0)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
refine_1 : Eq.{v_1 + 1} (α := X ⟶ 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X ≫ 0)
refine_2 :
  Eq.{v_1 + 1} (α := 0 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (CategoryStruct.comp (Y := 0) 0 0) 0
refine_3 : Eq.{v_1 + 1} (α := X ⟶ 0) (CategoryStruct.comp (Y := 0) 0 0) 0
refine_4 :
  Eq.{v_1 + 1} (α := 0 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 X)) (CategoryStruct.comp (Y := 0) 0 0)
⊢ Nonempty.{v_1 + 1} (Octahedron ⋯ ⋯ ⋯ ⋯)

Tactic:
refine ⟨⟨0, 0, ?_, ?_, ?_, ?_, isomorphic_distinguished _ (contractible_distinguished (0 : C)) _
    (Triangle.isoMk _ _ (by rfl) (by rfl) (by rfl))⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X ≫ 0)

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := 0 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (CategoryStruct.comp (Y := 0) 0 0) 0

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ 0) (CategoryStruct.comp (Y := 0) 0 0) 0

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := 0 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 X)) (CategoryStruct.comp (Y := 0) 0 0)

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
dsimp : u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃
⊢ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁ ≫ u₂₃ = 𝟙 X₁ ≫ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
rw : u₁₂ ≫ u₂₃ = u₁₃
rw₁ rw₂ : u₁₃ = u₁₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃

Tactic:
rw [id_comp, comm]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
dsimp : w₁₂ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 X₁) = h.m₁ ≫ w₁₃
⊢ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 X₁) =
    h.m₁ ≫ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ w₁₂ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 X₁) = h.m₁ ≫ w₁₃

Tactic:
simpa only [Functor.map_id, comp_id] using h.comm₂.symm

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Triangulated.Octahedron.comm₂, Eq.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
dsimp : u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁ ≫ 𝟙 X₃ = u₁₂ ≫ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
rw : u₁₃ = u₁₂ ≫ u₂₃
rw₁ rw₂ : u₁₃ = u₁₃
⊢ u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃

Tactic:
rw [comp_id, comm]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
dsimp : v₁₃ ≫ h.m₃ = 𝟙 X₃ ≫ v₂₃
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂ ≫ h.m₃ = 𝟙 X₃ ≫ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
rw : v₁₃ ≫ h.m₃ = v₂₃
rw₁ rw₂ : v₂₃ = v₂₃
⊢ v₁₃ ≫ h.m₃ = 𝟙 X₃ ≫ v₂₃

Tactic:
rw [id_comp, h.comm₃]

Premises used: CategoryTheory.Triangulated.Octahedron.comm₃, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ 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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃' v₁₃' w₁₃')
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
iso₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ≅ Triangle.mk u₁₂' v₁₂' w₁₂' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂
iso₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ≅ Triangle.mk u₂₃' v₂₃' w₂₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃
dsimp : u₁₃ ≫ e₃.hom = e₁.hom ≫ u₁₃'
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁ ≫ e₃.hom = e₁.hom ≫ (Triangle.mk u₁₃' v₁₃' w₁₃').mor₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Triangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ 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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (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_2 _ inst_1 inst_4 _)
    (Triangle.mk u₁₃' v₁₃' w₁₃')
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
iso₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ≅ Triangle.mk u₁₂' v₁₂' w₁₂' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂
iso₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ≅ Triangle.mk u₂₃' v₂₃' w₂₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃
rw : (u₁₂ ≫ u₂₃) ≫ e₃.hom = e₁.hom ≫ u₁₃'
rw₁ : u₁₂ ≫ u₂₃ ≫ e₃.hom = e₁.hom ≫ u₁₃'
rw₂ : u₁₂ ≫ u₂₃ ≫ e₃.hom = e₁.hom ≫ u₁₂' ≫ u₂₃'
rw₃ : u₁₂ ≫ u₂₃ ≫ e₃.hom = u₁₂ ≫ e₂.hom ≫ u₂₃'
rw₄ rw₅ : u₁₂ ≫ e₂.hom ≫ u₂₃' = u₁₂ ≫ e₂.hom ≫ u₂₃'
⊢ u₁₃ ≫ e₃.hom = e₁.hom ≫ u₁₃'

Tactic:
rw [← comm, assoc, ← comm', ← reassoc_of% comm₁₂, comm₂₃]

Premises used: CategoryTheory.Category.assoc