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 ℤ
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₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ =
    e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ =
    e₁.inv.hom₃ ≫ T₁.mor₃
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  Eq (α := L.obj T₁'.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj T₂'.obj₁))
    (L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁)
    (φ.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁)
refine_1 : T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_2 : T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = (e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃) ≫ 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:
refine ⟨e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃, ?_, ?_⟩
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
⊢ L.mapArrow.EssSurj

Tactic:
have := essSurj_mapArrow L W
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
⊢ ∃ (φ : Arrow.{v_1, u_1} C), Nonempty.{v_2 + 1} (L.mapArrow.obj φ ≅ Arrow.mk f)

Tactic:
⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
obtain :
  ∀ (φ : Arrow.{v_1, u_1} C) (e : L.mapArrow.obj φ ≅ Arrow.mk f),
    ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)

Tactic:
obtain ⟨φ, ⟨e⟩⟩ : ∃ (φ : Arrow C), Nonempty (L.mapArrow.obj φ ≅ Arrow.mk f) :=
    ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Premises used: CategoryTheory.Arrow
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
obtain :
  ∀ (Z : C) (g : φ.right ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left)
    (H :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
        (Triangle.mk φ.hom g h)),
    ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)

Tactic:
obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle φ.hom

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)

Tactic:
⟨L.obj Z, e.inv.right ≫ L.map g,
    L.map h ≫ (L.commShiftIso (1 : ℤ)).hom.app _ ≫ e.hom.left⟦(1 : ℤ)⟧', _, ?_, H⟩

Premises used: CategoryTheory.Arrow.Hom.right, CategoryTheory.shiftFunctor, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.Hom.left, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
refine :
  Iso (C := Triangle.{v_2, u_2} D)
    (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
      (L.map h ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
          Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)))
    (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)

Tactic:
refine ⟨L.obj Z, e.inv.right ≫ L.map g,
    L.map h ≫ (L.commShiftIso (1 : ℤ)).hom.app _ ≫ e.hom.left⟦(1 : ℤ)⟧', _, ?_, H⟩
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
⊢ Triangle.mor₂
        (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
          (L.map h ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
              Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₃
            (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
              (L.map h ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
                  Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))))) =
    Iso.hom (Functor.mapIso Arrow.rightFunc e.symm) ≫ Triangle.mor₂ (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))

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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
refine :
  Triangle.mor₃
        (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
          (L.map h ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
              Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Functor.mapIso Arrow.leftFunc e.symm)) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₃
            (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
              (L.map h ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
                  Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))))) ≫
      Triangle.mor₃ (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))
⊢ Iso (C := Triangle.{v_2, u_2} D)
    (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
      (L.map h ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
          Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)))
    (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))

Tactic:
refine Triangle.isoMk _ _ (Arrow.leftFunc.mapIso e.symm) (Arrow.rightFunc.mapIso e.symm)
    (Iso.refl _) e.inv.w.symm (by simp) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
dsimp :
  Eq (α := L.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj φ.left))
    ((L.map h ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
          Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) e.inv.left)
    (𝟙 (L.obj Z) ≫ L.map h ≫ NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left)
⊢ Triangle.mor₃
        (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
          (L.map h ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
              Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Functor.mapIso Arrow.leftFunc e.symm)) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₃
            (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
              (L.map h ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
                  Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))))) ≫
      Triangle.mor₃ (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))

Tactic:
dsimp
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
⊢ Eq (α := L.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj φ.left))
    ((L.map h ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
          Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) e.inv.left)
    (𝟙 (L.obj Z) ≫ L.map h ≫ NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left)

Tactic:
simp only [assoc, id_comp, ← Functor.map_comp, ← Arrow.comp_left, e.hom_inv_id, Arrow.id_left,
    Functor.mapArrow_obj, Arrow.mk_left, Functor.map_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapArrow_obj, CategoryTheory.Arrow.comp_left, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Arrow.id_left, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Arrow.mk_left, CategoryTheory.Category.id_comp
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
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₁
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
L.complete_distinguished_essImageDistTriang_morphism ?_ T₁ T₂ hT₁ hT₂ a b fac

Premises used: CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
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₁
refine :
  ∀ (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) (Functor.obj L.mapTriangle T₁') (Functor.obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
refine L.complete_distinguished_essImageDistTriang_morphism ?_ T₁ T₂ hT₁ hT₂ a b fac

Premises used: CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : 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₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
obtain :
  ∀ (α : W.LeftFraction T₁.obj₁ T₂.obj₁) (hα : a = α.map (W := W) L ⋯),
    ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
      φ.hom₁ = a ∧ φ.hom₂ = b
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
obtain ⟨α, hα⟩ := exists_leftFraction L W a

Premises used: CategoryTheory.Localization.exists_leftFraction
-- 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 : ℤ), Functor.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 ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : 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₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
obtain :
  ∀ (β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂)
    (hβ :
      (MorphismProperty.RightFraction.mk (W := W) (α.s (W := W)) ⋯ T₂.mor₁).f (W := W) ≫ β.s (W := W) =
        (MorphismProperty.RightFraction.mk (W := W) (α.s (W := W)) ⋯ T₂.mor₁).s (W := W) ≫ β.f (W := W)),
    ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
      φ.hom₁ = a ∧ φ.hom₂ = b
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
obtain ⟨β, hβ⟩ := (MorphismProperty.RightFraction.mk α.s α.hs T₂.mor₁).exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.Pretriangulated.Triangle.mor₁