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 : ℤ), 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 ⋯
β : 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)
obtain :
  ∀ (γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))) (hγ : b ≫ L.map (β.s (W := W)) = γ.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 (b ≫ L.map β.s)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Localization.exists_leftFraction, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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 ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
rw :
  ∀ (hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)) (γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W)))
    (fac :
      L.map (T₁.mor₁ ≫ γ.f (W := W)) = α.map (W := W) L ⋯ ≫ L.map T₂.mor₁ ≫ L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)))
    (hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯),
    L.map (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) = L.map (T₁.mor₁ ≫ γ.f (W := W))
⊢ L.map (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) = L.map (T₁.mor₁ ≫ γ.f (W := W))

Tactic:
rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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 ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
obtain :
  ∀ (Z₂ : C) (σ : γ.Y' (W := W) ⟶ Z₂) (hσ : W σ)
    (fac : (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) ≫ σ = (T₁.mor₁ ≫ γ.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 ⟨Z₂, σ, hσ, fac⟩ := (MorphismProperty.map_eq_iff_postcomp L W
    (α.f ≫ β.f ≫ γ.s) (T₁.mor₁ ≫ γ.f)).1 (by
      rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac
      rw [fac, ← Functor.map_comp_assoc, hβ, Functor.map_comp, Functor.map_comp,
        Functor.map_comp, assoc, MorphismProperty.LeftFraction.map_comp_map_s_assoc])

Premises used: CategoryTheory.MorphismProperty.map_eq_iff_postcomp, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.Pretriangulated.Triangle.mor₁
-- 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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) ≫ σ = (T₁.mor₁ ≫ γ.f (W := W)) ≫ σ
⊢ α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ

Tactic:
simp only [assoc] at fac

Premises used: CategoryTheory.Category.assoc
-- 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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
obtain :
  ∀ (Y₃ : C) (g : Z₂ ⟶ Y₃) (h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W)))
    (hT₃ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
        (Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h)),
    ∃ (φ : 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 ⟨Y₃, g, h, hT₃⟩ := Pretriangulated.distinguished_cocone_triangle (β.f ≫ γ.s ≫ σ)

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
hT₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h)
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃

Tactic:
change T₃ ∈ distTriang C at 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 : ℤ), 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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
⊢ W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)

Tactic:
have hβγσ : W (β.s ≫ γ.s ≫ σ) := W.comp_mem _ _ β.hs (W.comp_mem _ _ γ.hs 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
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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
dsimp : T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
⊢ T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ T₃.mor₁

Tactic:
dsimp [T₃]
-- 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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
rw rw₁ : α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
⊢ T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ

Tactic:
rw [reassoc_of% 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
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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
obtain :
  ∀ (ψ₃ : T₂.obj₃ ⟶ T₃.obj₃) (hψ₃ : W ψ₃) (hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ≫ T₃.mor₂)
    (hψ₂ : T₂.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (α.s (W := W)) = ψ₃ ≫ 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
⊢ ∃ (φ : 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ψ₃, hψ₁, hψ₂⟩ := MorphismProperty.compatible_with_triangulation
    T₂ T₃ hT₂ hT₃ α.s (β.s ≫ γ.s ≫ σ) α.hs hβγσ (by dsimp [T₃]; rw [reassoc_of% hβ])

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation
-- 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_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (α.s (W := W)) = ψ₃ ≫ T₃.mor₃
dsimp : T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
⊢ T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ T₃.mor₁

Tactic:
dsimp [T₃]