ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle D<VAR>hT₁ : T₁ ∈ L.essImageDistTriang<VAR>hT₂ : T₂ ∈ L.essImageDistTriang<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle D<VAR>hT₁ : T₁ ∈ L.essImageDistTriang<VAR>hT₂ : T₂ ∈ L.essImageDistTriang<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (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₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).f ≫ β.s = (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).s ≫ β.f<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).f ≫ β.s = (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).f ≫ β.s = (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this : IsIso (L.map β.s)<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).f ≫ β.s = (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : (α.f ≫ β.f ≫ γ.s) ≫ σ = (T₁.mor₁ ≫ γ.f) ≫ σ<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>hT₃ : Triangle.mk (β.f ≫ γ.s ≫ σ) g h ∈ distinguishedTriangles<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<VAR>hβγσ : W (β.s ≫ γ.s ≫ σ)<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<VAR>hβγσ : W (β.s ≫ γ.s ≫ σ)<VAR>ψ₃ : T₂.obj₃ ⟶ T₃.obj₃<VAR>hψ₃ : W ψ₃<VAR>hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂<VAR>hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝ : IsIso (L.map β.s)<VAR>this : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<VAR>hβγσ : W (β.s ≫ γ.s ≫ σ)<VAR>ψ₃ : T₂.obj₃ ⟶ T₃.obj₃<VAR>hψ₃ : W ψ₃<VAR>hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂<VAR>hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃<VAR>ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝¹ : IsIso (L.map β.s)<VAR>this✝ : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<VAR>hβγσ : W (β.s ≫ γ.s ≫ σ)<VAR>ψ₃ : T₂.obj₃ ⟶ T₃.obj₃<VAR>hψ₃ : W ψ₃<VAR>hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂<VAR>hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃<VAR>ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂<VAR>this : IsIso (L.mapTriangle.map ψ)<GOAL>∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁<VAR>b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂<VAR>fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁<VAR>α : W.LeftFraction T₁.obj₁ T₂.obj₁<VAR>hα : a = α.map L ⋯<VAR>β : W.LeftFraction α.Y' T₂.obj₂<VAR>hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f<VAR>γ : W.LeftFraction T₁.obj₂ β.Y'<VAR>hγ : b ≫ L.map β.s = γ.map L ⋯<VAR>this✝¹ : IsIso (L.map β.s)<VAR>this✝ : IsIso (L.map γ.s)<VAR>Z₂ : C<VAR>σ : γ.Y' ⟶ Z₂<VAR>hσ : W σ<VAR>fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ<VAR>Y₃ : C<VAR>g : Z₂ ⟶ Y₃<VAR>h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'<VAR>T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h<VAR>hT₃ : T₃ ∈ distinguishedTriangles<VAR>hβγσ : W (β.s ≫ γ.s ≫ σ)<VAR>ψ₃ : T₂.obj₃ ⟶ T₃.obj₃<VAR>hψ₃ : W ψ₃<VAR>hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂<VAR>hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃<VAR>ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂<VAR>this : IsIso (L.mapTriangle.map ψ)<GOAL>(L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫ inv (L.mapTriangle.map ψ)).hom₁ = a