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_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₃
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) ≫ σ)
ψ₃ : 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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
⊢ IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)

Tactic:
have : IsIso (L.mapTriangle.map ψ) := Triangle.isIso_of_isIsos _
    (inverts L W α.s α.hs) (inverts L W _ hβγσ) (inverts L W ψ₃ 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) ≫ σ)
ψ₃ : 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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
⟨L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f
      (γ.f ≫ σ) fac.symm) ≫ inv (L.mapTriangle.map ψ), ?_, ?_⟩

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.mapTriangle, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.inv, Eq.symm, CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism
-- 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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
refine_1 :
  TriangleMorphism.hom₁
      (Functor.map L.mapTriangle
          (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯) ≫
        inv (Functor.map L.mapTriangle ψ)) =
    a
refine_2 :
  TriangleMorphism.hom₂
      (Functor.map L.mapTriangle
          (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯) ≫
        inv (Functor.map L.mapTriangle ψ)) =
    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:
refine ⟨L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f
      (γ.f ≫ σ) fac.symm) ≫ inv (L.mapTriangle.map ψ), ?_, ?_⟩
-- 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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
refine_1 :
  Eq (α := Triangle.obj₁ (Functor.obj L.mapTriangle T₁) ⟶ Triangle.obj₁ (Functor.obj L.mapTriangle T₃))
    (TriangleMorphism.hom₁
      (Functor.map L.mapTriangle
        (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯)))
    (a ≫ TriangleMorphism.hom₁ (Functor.map L.mapTriangle ψ))
⊢ TriangleMorphism.hom₁
      (Functor.map L.mapTriangle
          (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯) ≫
        inv (Functor.map L.mapTriangle ψ)) =
    a

Tactic:
rw [← cancel_mono (L.mapTriangle.map ψ).hom₁, ← comp_hom₁, assoc, IsIso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁, CategoryTheory.Pretriangulated.comp_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
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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
refine_1 : L.map (α.f (W := W)) = a ≫ L.map (α.s (W := W))
⊢ Eq (α := Triangle.obj₁ (Functor.obj L.mapTriangle T₁) ⟶ Triangle.obj₁ (Functor.obj L.mapTriangle T₃))
    (TriangleMorphism.hom₁
      (Functor.map L.mapTriangle
        (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯)))
    (a ≫ TriangleMorphism.hom₁ (Functor.map L.mapTriangle ψ))

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
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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
refine_1 : L.map (α.f (W := W)) = α.map (W := W) L ⋯ ≫ L.map (α.s (W := W))
refine_1₁ refine_1₂ : L.map (α.f (W := W)) = L.map (α.f (W := W))
⊢ L.map (α.f (W := W)) = a ≫ L.map (α.s (W := W))

Tactic:
rw [hα, MorphismProperty.LeftFraction.map_comp_map_s]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_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))
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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
refine_2 :
  Eq (α := Triangle.obj₂ (Functor.obj L.mapTriangle T₁) ⟶ Triangle.obj₂ (Functor.obj L.mapTriangle T₃))
    (TriangleMorphism.hom₂
      (Functor.map L.mapTriangle
        (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯)))
    (b ≫ TriangleMorphism.hom₂ (Functor.map L.mapTriangle ψ))
⊢ TriangleMorphism.hom₂
      (Functor.map L.mapTriangle
          (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯) ≫
        inv (Functor.map L.mapTriangle ψ)) =
    b

Tactic:
rw [← cancel_mono (L.mapTriangle.map ψ).hom₂, ← comp_hom₂, assoc, IsIso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.comp_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
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₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
refine_2 : L.map (γ.f (W := W) ≫ σ) = b ≫ L.map (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
⊢ Eq (α := Triangle.obj₂ (Functor.obj L.mapTriangle T₁) ⟶ Triangle.obj₂ (Functor.obj L.mapTriangle T₃))
    (TriangleMorphism.hom₂
      (Functor.map L.mapTriangle
        (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ (α.f (W := W)) (γ.f (W := W) ≫ σ) ⋯)))
    (b ≫ TriangleMorphism.hom₂ (Functor.map L.mapTriangle ψ))

Tactic:
dsimp [ψ]