awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (contractibleTriangle X)

Tactic:
⟨contractibleTriangle (L.objPreimage X), ?_, contractible_distinguished _⟩

Premises used: Set.Mem, setOf, CategoryTheory.Functor.objPreimage, Exists.intro, CategoryTheory.Functor.essImageDistTriang, CategoryTheory.Pretriangulated.contractible_distinguished, CategoryTheory.Pretriangulated.contractibleTriangle
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
refine :
  Iso (C := Triangle.{v_2, u_2} D) (contractibleTriangle X)
    (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X)))
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (contractibleTriangle X)

Tactic:
refine ⟨contractibleTriangle (L.objPreimage X), ?_, contractible_distinguished _⟩
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
⊢ Triangle.mor₁ (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X))) ≫
      Iso.hom (Iso.refl (Triangle.obj₂.{v_2, u_2} (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X))))) =
    Iso.hom (Iso.refl (Triangle.obj₁.{v_2, u_2} (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X))))) ≫
      Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
⊢ Triangle.mor₂ (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X))) ≫ Iso.hom (Iso.symm L.mapZeroObject) =
    Iso.hom (Iso.refl (Triangle.obj₂.{v_2, u_2} (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X))))) ≫
      Triangle.mor₂ (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
⊢ Triangle.mor₃ (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X))) ≫
      map (shiftFunctor D (A := ℤ) 1)
        (Iso.hom
          (Iso.refl (Triangle.obj₁.{v_2, u_2} (obj (contractibleTriangleFunctor D) (L.obj (L.objPreimage X)))))) =
    CategoryStruct.comp (Y :=
      Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X))))
      (Iso.hom (Iso.symm L.mapZeroObject))
      (Triangle.mor₃ (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
⊢ Iso (C := Triangle.{v_2, u_2} D) (contractibleTriangle X)
    (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X)))

Tactic:
exact ((contractibleTriangleFunctor D).mapIso (L.objObjPreimageIso X)).symm ≪≫
    Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) L.mapZeroObject.symm (by simp) (by simp) (by simp)

Premises used: CategoryTheory.Pretriangulated.contractibleTriangleFunctor, CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
mp :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T →
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate
mpr :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate →
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
T' : Triangle.{v_1, u_1} C
e' : T ≅ obj L.mapTriangle T'
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate

Tactic:
⟨T'.rotate, (rotate D).mapIso e' ≪≫ L.mapTriangleRotateIso.app T',
      rot_of_distTriang T' hT'⟩

Premises used: Set.Mem, setOf, CategoryTheory.Pretriangulated.Triangle.rotate, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Pretriangulated.rotate, CategoryTheory.Functor.essImageDistTriang, CategoryTheory.Pretriangulated.rot_of_distTriang, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.mapTriangleRotateIso
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
T' : Triangle.{v_1, u_1} C
e' : T ≅ obj L.mapTriangle T'
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate

Tactic:
exact ⟨T'.rotate, (rotate D).mapIso e' ≪≫ L.mapTriangleRotateIso.app T',
      rot_of_distTriang T' hT'⟩
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
T' : Triangle.{v_1, u_1} C
e' : T.rotate ≅ obj L.mapTriangle T'
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
⟨T'.invRotate, (triangleRotation D).unitIso.app T ≪≫ (invRotate D).mapIso e' ≪≫
      L.mapTriangleInvRotateIso.app T', inv_rot_of_distTriang T' hT'⟩

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Pretriangulated.triangleRotation, Set.Mem, CategoryTheory.Pretriangulated.Triangle.invRotate, setOf, CategoryTheory.Functor.mapTriangleInvRotateIso, CategoryTheory.Iso.trans, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Exists.intro, CategoryTheory.Functor.essImageDistTriang, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Pretriangulated.invRotate
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
T' : Triangle.{v_1, u_1} C
e' : T.rotate ≅ obj L.mapTriangle T'
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
exact ⟨T'.invRotate, (triangleRotation D).unitIso.app T ≪≫ (invRotate D).mapIso e' ≪≫
      L.mapTriangleInvRotateIso.app T', inv_rot_of_distTriang T' hT'⟩
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
hT₁ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
obtain :
  ∀ (T₁' : Triangle.{v_1, u_1} C) (e₁ : T₁ ≅ obj L.mapTriangle T₁')
    (hT₁' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
obtain ⟨T₁', e₁, hT₁'⟩ := hT₁
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
hT₂ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
obtain :
  ∀ (T₂' : Triangle.{v_1, u_1} C) (e₂ : T₂ ≅ obj L.mapTriangle T₂')
    (hT₂' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
obtain ⟨T₂', e₂, hT₂'⟩ := hT₂
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
⊢ Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁

Tactic:
have comm₁ := e₁.inv.comm₁
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
⊢ T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')

Tactic:
have comm₁' := e₂.hom.comm₁
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₁')

Tactic:
have comm₂ := e₁.hom.comm₂
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂' →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₁')
⊢ T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₂')

Tactic:
have comm₂' := e₂.hom.comm₂