awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : A.IsVerdierRightLocalizing B
X Y : Cᵒᵖ
f : X ⟶ Y
hX : A.op X
hY : B.op Y
Z : C
a : unop Y ⟶ Z
b : Z ⟶ unop X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.unop
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩

Premises used: Quiver.Hom.op, Quiver.Hom.unop_inj, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : A.IsVerdierRightLocalizing B
X Y : Cᵒᵖ
f : X ⟶ Y
hX : A.op X
hY : B.op Y
Z : C
a : unop Y ⟶ Z
b : Z ⟶ unop X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.unop
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 : IsVerdierRightLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : A.unop X
hY : B.unop Y
obtain :
  ∀ (Z : Cᵒᵖ) (a : op Y ⟶ Z) (b : Z ⟶ op X) (h₁ : A Z) (h₂ : B Z) (fac : a ≫ b = f.op),
    ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.op hY hX

Premises used: Quiver.Hom.op, CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 : IsVerdierRightLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : A.unop X
hY : B.unop Y
Z : Cᵒᵖ
a : op Y ⟶ Z
b : Z ⟶ op X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.op
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 : IsVerdierRightLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : A.unop X
hY : B.unop Y
Z : Cᵒᵖ
a : op Y ⟶ Z
b : Z ⟶ op X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.op
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
⊢ IsVerdierLeftLocalizing.{v_1, u_1} A.op B.op ↔ A.IsVerdierRightLocalizing B

Tactic:
⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierRightLocalizing B.op.unop),
    fun _ ↦ inferInstance⟩

Premises used: inferInstance, _private.0.CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_op_iff._proof_1, Iff.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
⊢ IsVerdierRightLocalizing.{v_1, u_1} A.op B.op ↔ A.IsVerdierLeftLocalizing B

Tactic:
⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierLeftLocalizing B.op.unop),
    fun _ ↦ inferInstance⟩

Premises used: _private.0.CategoryTheory.ObjectProperty.isVerdierRightLocalizing_op_iff._proof_1, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
⊢ A.IsVerdierRightLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩

Premises used: CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
refine_1 :
  A.IsVerdierRightLocalizing B →
    ∀ (X Y : C) (s : X ⟶ Y) (hX : A X) (hs : B.trW s),
      ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
refine_2 :
  ∀
    (hA :
      ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s')
    {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y), ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f
⊢ A.IsVerdierRightLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
hs : B.trW s
⊢ ∃ (X_1 : C) (f : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s h)),
    B X_1

Tactic:
rw [ObjectProperty.trW_iff'] at hs

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
hs :
  ∃ (X_1 : C) (f : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s h)),
    B X_1
refine_1 :
  ∀ (W : C) (a : W ⟶ X) (b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b))
    (hW : B W), ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
⊢ ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨W, a, b, hT, hW⟩ := hs
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
refine_1 :
  ∀ (W' : C) (c : W ⟶ W') (d : W' ⟶ X) (h₁ : A W') (h₂ : B W') (fac : c ≫ d = a),
    ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
⊢ ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac a hW hX

Premises used: CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
refine_1 :
  ∀ (U : C) (hU : A U) (e : X ⟶ U) (f : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W')
    (hT' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk d e f)),
    ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
⊢ ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX

Premises used: CategoryTheory.ObjectProperty.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W'
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk d e f)
refine_1 :
  ∀ (g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃)
    (hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂),
    (Triangle.mk a s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c = g ≫ (Triangle.mk d e f).mor₃ →
      ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
⊢ ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT'
      c (𝟙 _) (by cat_disch)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W'
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk d e f)
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right : (Triangle.mk a s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c = g ≫ (Triangle.mk d e f).mor₃
refine_1 : (A ⊓ B).trW e
⊢ ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'

Tactic:
refine ⟨U, e, g, hU, ?_, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W'
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk d e f)
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right : (Triangle.mk a s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c = g ≫ (Triangle.mk d e f).mor₃
refine_1 :
  ∃ (X_1 : C) (f : X_1 ⟶ X) (h : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f e h)),
    (A ⊓ B) X_1
⊢ (A ⊓ B).trW e

Tactic:
rw [ObjectProperty.trW_iff']

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W'
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk d e f)
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right : (Triangle.mk a s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c = g ≫ (Triangle.mk d e f).mor₃
⊢ ∃ (X_1 : C) (f : X_1 ⟶ X) (h : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f e h)),
    (A ⊓ B) X_1

Tactic:
⟨_, _, _, hT', h₁, h₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
W : C
a : W ⟶ X
b : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s b)
hW : B W
W' : C
c : W ⟶ W'
d : W' ⟶ X
h₁ : A W'
h₂ : B W'
fac : c ≫ d = a
U : C
hU : A U
e : X ⟶ U
f : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) W'
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk d e f)
g : (Triangle.mk a s b).obj₃ ⟶ (Triangle.mk d e f).obj₃
hg : (Triangle.mk a s b).mor₂ ≫ g = 𝟙 (Triangle.mk a s b).obj₂ ≫ (Triangle.mk d e f).mor₂
right : (Triangle.mk a s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c = g ≫ (Triangle.mk d e f).mor₃
⊢ ∃ (X_1 : C) (f : X_1 ⟶ X) (h : U ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f e h)),
    (A ⊓ B) X_1

Tactic:
exact ⟨_, _, _, hT', h₁, h₂⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
refine_2 :
  ∀ (Z : C) (s : Y ⟶ Z) (b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s b)),
    ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, s, b, hT⟩ := Pretriangulated.distinguished_cocone_triangle f

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s b)
rw :
  ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s h)),
    B X
⊢ B.trW s

Tactic:
rw [trW_iff']

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s b)
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s h)),
    B X

Tactic:
⟨_, _, _, hT, hX⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s b)
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s h)),
    B X

Tactic:
exact ⟨_, _, _, hT, hX⟩