awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_1 :
  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁) =
    v₁₂
⊢ m₁ ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) Z₁₃)
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁) =
    v₁₂

Tactic:
dsimp [m₁]
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_1 :
  NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁ =
    v₁₂
⊢ (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁) =
    v₁₂

Tactic:
rw [assoc, assoc, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app_assoc
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_1 :
  NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
      (Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
          Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁ =
    v₁₂
⊢ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁ =
    v₁₂

Tactic:
nth_rw 2 [← assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_1 :
  NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1)) (o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁ =
    v₁₂
refine_1₁ :
  CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂)
      (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁) =
    v₁₂
refine_1₂ refine_1₃ : v₁₂ = v₁₂
⊢ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
      (Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
          Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₁ =
    v₁₂

Tactic:
rw [← Functor.map_comp, eq₂, shiftFunctorCompIsoId_naturality_1]

Premises used: CategoryTheory.shiftFunctorCompIsoId_naturality_1, CategoryTheory.Functor.map_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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_2 :
  w₁₂ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₂ ≫
          Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃) =
    u₂₃ ≫ w₁₃
⊢ w₁₂ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) m₁ = u₂₃ ≫ w₁₃

Tactic:
dsimp [m₁]
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_3 :
  w₁₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃) =
    w₂₃
⊢ w₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = w₂₃

Tactic:
dsimp [m₃]
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_4 :
  m₃ ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) Z₂₃)
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂) =
    v₁₃ ≫ u₁₂
⊢ m₃ ≫ v₂₃ = v₁₃ ≫ u₁₂

Tactic:
rw [← shiftFunctorCompIsoId_naturality_1 v₂₃ 1 (-1) (Int.add_right_neg 1)]

Premises used: CategoryTheory.shiftFunctorCompIsoId_naturality_1, Int.add_right_neg, OfNat.ofNat, Neg.neg
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_4 :
  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂) =
    v₁₃ ≫ u₁₂
⊢ m₃ ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) Z₂₃)
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂) =
    v₁₃ ≫ u₁₂

Tactic:
dsimp [m₃]
-- 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
inst_6 : IsTriangulated.{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₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ = Functor.map (shiftFunctor C (A := ℤ) 1) v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ :
  Functor.map (shiftFunctor C (A := ℤ) 1) v₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
    o.m₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃
refine_4 :
  NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂ =
    v₁₃ ≫ u₁₂
⊢ (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₁₃ ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) Z₂₃)
        (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) v₂₃) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X₂) =
    v₁₃ ≫ u₁₂

Tactic:
rw [assoc, assoc, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app_assoc