awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) T₁.obj₁ ⟶
      Functor.obj.{v, v, u, u} (𝟭 C) T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) e₁.hom ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ Functor.map (𝟭 C) e₁.hom)
dsimp :
  Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁) ≫
        e₁.hom :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
⊢ Iso.hom (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) ≫ (Arrow.mk T₂.invRotate.mor₁).hom =
    (Arrow.mk T₁.invRotate.mor₁).hom ≫ e₁.hom

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
      T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
        T₂.obj₁)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ e₁.hom :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
        T₂.obj₁)
simp :
  Functor.map (shiftFunctor C (A := ℤ) (-1)) (T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁ =
    Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ e₁.hom
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁) ≫
        e₁.hom :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)

Tactic:
simp only [comp_neg, neg_comp, assoc, neg_inj, ← Functor.map_comp_assoc, ← comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Functor.map_comp_assoc, neg_inj, CategoryTheory.Preadditive.neg_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
      T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
        T₂.obj₁)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ e₁.hom :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
        T₂.obj₁)
⊢ Functor.map (shiftFunctor C (A := ℤ) (-1)) (T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁ =
    Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ e₁.hom

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
⊢ ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))

Tactic:
have h := exists_iso_of_arrow_iso _ _ (inv_rot_of_distTriang _ hT₁)
    (inv_rot_of_distTriang _ hT₂)
    (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ (by
      have := (shiftFunctorCompIsoId C (1 : ℤ) (-1) (by simp)).hom.naturality e₁.hom
      dsimp at this ⊢
      simp only [comp_neg, neg_comp, assoc, neg_inj, ← Functor.map_comp_assoc, ← comm]
      simp [this]))
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
⊢ e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))

Tactic:
have h₁ : e.hom.hom₁ = _ := h.choose_spec.1
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
⊢ Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) = e.hom.hom₂

Tactic:
have h₂ : _ = e.hom.hom₂ := h.choose_spec.2.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
h₂ : Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) = e.hom.hom₂
⊢ T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃

Tactic:
have h₃ := e.hom.comm₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
h₂ : Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) = e.hom.hom₂
h₃ : T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
⊢ HAdd.hAdd (α := ℤ) (-1) 1 = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
h₂ : Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) = e.hom.hom₂
h₃ : T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (𝟭 C) T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1) T₂.obj₃)
    (Functor.map (𝟭 C) e₃.hom ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1) e₃.hom)

Tactic:
have h₄ := (shiftFunctorCompIsoId C (-1 : ℤ) 1 (by simp)).inv.naturality e₃.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₁.3) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₂.3
h₄ :
  Eq (α :=
    T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (e₃.hom ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom))
refine_1 : T₁.mor₁ ≫ Iso.hom (Functor.mapIso Triangle.π₃ e) = e₁.hom ≫ T₂.mor₁
refine_2 : T₁.mor₂ ≫ e₃.hom = Iso.hom (Functor.mapIso Triangle.π₃ e) ≫ T₂.mor₂
⊢ T₁ ≅ T₂

Tactic:
refine Triangle.isoMk _ _ e₁ (Triangle.π₃.mapIso e) e₃ ?_ ?_ comm

Premises used: CategoryTheory.Pretriangulated.Triangle.π₃, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₁.3) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₂.3
h₄ :
  Eq (α :=
    T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (e₃.hom ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom))
⊢ T₁.invRotate.mor₂ ≫ e.hom.hom₃ = e.hom.hom₂ ≫ T₂.invRotate.mor₂

Tactic:
e.hom.comm₂

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₁.3) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₂.3
h₄ :
  Eq (α :=
    T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (e₃.hom ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom))
⊢ T₁.mor₁ ≫ Iso.hom (Functor.mapIso Triangle.π₃ e) = e₁.hom ≫ T₂.mor₁

Tactic:
convert! e.hom.comm₂ using 2

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂