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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this : IsIso φ.hom₁
⊢ IsIso (Arrow.Hom.right e.hom)

Tactic:
infer_instance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this : IsIso φ.hom₁
⊢ IsIso φ.hom₂

Tactic:
have : IsIso φ.hom₂ := by dsimp [φ]; infer_instance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this : IsIso φ.hom₂
⊢ IsIso φ.hom₃

Tactic:
have : IsIso φ.hom₃ := isIso₃_of_isIso₁₂ φ hT₁ hT₂ inferInstance inferInstance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this : IsIso φ.hom₃
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso φ

Tactic:
apply Triangle.isIso_of_isIsos

Premises used: CategoryTheory.Pretriangulated.Triangle.isIso_of_isIsos
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ IsIso φ.hom₁

Tactic:
infer_instance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ IsIso φ.hom₂

Tactic:
infer_instance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ IsIso φ.hom₃

Tactic:
infer_instance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this : IsIso φ.hom₃
⊢ IsIso φ

Tactic:
have : IsIso φ := by
    apply Triangle.isIso_of_isIsos
    all_goals infer_instance
-- 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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this_3 : IsIso φ.hom₃
this : IsIso φ
⊢ (asIso φ).hom.hom₁ = Arrow.Hom.left e.hom

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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this_3 : IsIso φ.hom₃
this : IsIso φ
⊢ (asIso φ).hom.hom₂ = Arrow.Hom.right e.hom

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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this_1 : IsIso φ.hom₁
this_2 : IsIso φ.hom₂
this_3 : IsIso φ.hom₃
this : IsIso φ
⊢ ∃ (e' : T₁ ≅ T₂), e'.hom.hom₁ = Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = Arrow.Hom.right e.hom

Tactic:
exact ⟨asIso φ, by simp [φ], by 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
⊢ ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))

Tactic:
have h := exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk e₁ e₂ comm.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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ h.choose (p := fun (e' : T₁ ≅ T₂) ↦
          e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
            e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))).hom.hom₂ =
    Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))

Tactic:
have eq := h.choose_spec.2
-- 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq :
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦
          e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
            e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))).hom.hom₂ =
    Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
dsimp :
  T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
⊢ T₁.mor₂ ≫
      Iso.hom
        (Functor.mapIso Triangle.π₃
          (h.choose (p := fun (e' : T₁ ≅ T₂) ↦
            e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
              e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))))) =
    e₂.hom ≫ T₂.mor₂

Tactic:
dsimp at eq ⊢
-- 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₂ = e₂.hom
rw : T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃
| e₂.hom ≫ T₂.mor₂

Tactic:
rw [← eq, ← TriangleMorphism.comm₂]

Premises used: 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₂ = e₂.hom
conv_rhs :
  T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
conv_rhs₁ :
  T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ =
    T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃
⊢ T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂

Tactic:
conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]

Premises used: 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ h.choose (p := fun (e' : T₁ ≅ T₂) ↦
          e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
            e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))).hom.hom₁ =
    Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))

Tactic:
have eq := 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq :
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦
          e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
            e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))).hom.hom₁ =
    Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
dsimp :
  T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    Iso.hom
        (Functor.mapIso Triangle.π₃
          (h.choose (p := fun (e' : T₁ ≅ T₂) ↦
            e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
              e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))))) ≫
      T₂.mor₃

Tactic:
dsimp at eq ⊢
-- 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₁ = e₁.hom
rw : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
| T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom

Tactic:
rw [← eq, TriangleMorphism.comm₃]

Premises used: 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₁ = e₁.hom
conv_lhs :
  T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
conv_lhs₁ :
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃ =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃

Tactic:
conv_lhs => rw [← eq, TriangleMorphism.comm₃]

Premises used: 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₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ T₁ ≅ T₂

Tactic:
exact Triangle.isoMk _ _ e₁ e₂ (Triangle.π₃.mapIso h.choose) comm (by
    have eq := h.choose_spec.2
    dsimp at eq ⊢
    conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]) (by
    have eq := h.choose_spec.1
    dsimp at eq ⊢
    conv_lhs => rw [← eq, TriangleMorphism.comm₃])

Premises used: CategoryTheory.Pretriangulated.Triangle.π₃, CategoryTheory.Pretriangulated.Triangle.isoMk, Exists.choose, 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₃
⊢ 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₃
⊢ 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)

Tactic:
have := (shiftFunctorCompIsoId C (1 : ℤ) (-1) (by simp)).hom.naturality e₁.hom