awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ B.trW s

Tactic:
have hs : B.trW s := by
      rw [trW_iff']
      exact ⟨_, _, _, hT, hX⟩
-- 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)
hs : B.trW s
refine_2 :
  ∀ (W : C) (s' : Y ⟶ W) (g : Z ⟶ W) (hW : A W) (hs' : (A ⊓ B).trW s') (fac : s ≫ g = s'),
    ∃ (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 ⟨W, s', g, hW, hs', fac⟩ := hA s hY 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
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)
hs : B.trW s
W : C
s' : Y ⟶ W
g : Z ⟶ W
hW : A W
hs' : (A ⊓ B).trW s'
fac : s ≫ g = s'
refine_2 :
  ∀ (U : C) (hU : A U) (a : U ⟶ Y) (c : W ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) U)
    (hT' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s' c)),
    ∃ (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 ⟨U, hU, a, c, hT'⟩ := A.distinguished_cocone_triangle₁ s' hY hW

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
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)
hs : B.trW s
W : C
s' : Y ⟶ W
g : Z ⟶ W
hW : A W
hs' : (A ⊓ B).trW s'
fac : s ≫ g = s'
U : C
hU : A U
a : U ⟶ Y
c : W ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) U
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s' c)
refine_2 :
  ∀ (t : (Triangle.mk f s b).obj₁ ⟶ (Triangle.mk a s' c).obj₁)
    (ht : (Triangle.mk f s b).mor₁ ≫ 𝟙 Y = t ≫ (Triangle.mk a s' c).mor₁)
    (ht' : (Triangle.mk f s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) t = g ≫ (Triangle.mk a s' c).mor₃),
    ∃ (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 ⟨t, ht, ht'⟩ :=
      complete_distinguished_triangle_morphism₁ _ _ hT hT' (𝟙 Y) g (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
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)
hs : B.trW s
W : C
s' : Y ⟶ W
g : Z ⟶ W
hW : A W
hs' : (A ⊓ B).trW s'
fac : s ≫ g = s'
U : C
hU : A U
a : U ⟶ Y
c : W ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) U
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s' c)
t : (Triangle.mk f s b).obj₁ ⟶ (Triangle.mk a s' c).obj₁
ht : (Triangle.mk f s b).mor₁ ≫ 𝟙 Y = t ≫ (Triangle.mk a s' c).mor₁
ht' : (Triangle.mk f s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) t = g ≫ (Triangle.mk a s' c).mor₃
⊢ A ⊓ B ≤ B

Tactic:
simp
-- 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)
hs : B.trW s
W : C
s' : Y ⟶ W
g : Z ⟶ W
hW : A W
hs' : (A ⊓ B).trW s'
fac : s ≫ g = s'
U : C
hU : A U
a : U ⟶ Y
c : W ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) U
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk a s' c)
t : (Triangle.mk f s b).obj₁ ⟶ (Triangle.mk a s' c).obj₁
ht : (Triangle.mk f s b).mor₁ ≫ 𝟙 Y = t ≫ (Triangle.mk a s' c).mor₁
ht' : (Triangle.mk f s b).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) t = g ≫ (Triangle.mk a s' c).mor₃
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f

Tactic:
exact ⟨U, t, a, hU, (B.trW_iff_of_distinguished' _ hT').1 (trW_monotone (by simp) _ hs'),
      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
inst_9 : 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'

Tactic:
(isVerdierRightLocalizing_iff A B).1 inferInstance s hX hs

Premises used: inferInstance, Iff.mp, CategoryTheory.ObjectProperty.isVerdierRightLocalizing_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
rw :
  (∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y),
      A.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s') ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
⊢ A.IsVerdierLeftLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

Tactic:
rw [← isVerdierRightLocalizing_op_iff, isVerdierRightLocalizing_iff]

Premises used: CategoryTheory.ObjectProperty.isVerdierRightLocalizing_op_iff, CategoryTheory.ObjectProperty.isVerdierRightLocalizing_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
⊢ (∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y),
      A.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s') ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

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

Premises used: 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 :
  ∀
    (hA :
      ∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y),
        A.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s')
    (X Y : C) (s : X ⟶ Y) (hY : A Y) (hs : B.trW s),
    ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
refine_2 :
  ∀
    (hA :
      ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s')
    (X Y : Cᵒᵖ) (s : X ⟶ Y) (hX : A.op X) (hs : B.op.trW s),
    ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
⊢ (∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y),
      A.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s') ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

Tactic:
refine ⟨fun hA X Y s hY hs ↦ ?_, fun hA X Y s hX 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
hA :
  ∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y),
    A.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
⊢ trW.{v_1, u_1} B.op (X := op Y) (Y := op X) s.op

Tactic:
simpa [trW_op_iff]

Premises used: CategoryTheory.ObjectProperty.trW_op_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.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
refine_1 :
  ∀ (Z' : Cᵒᵖ) (s' : op Y ⟶ Z') (b : op X ⟶ Z') (hZ' : A.op Z') (hs' : (A.op ⊓ B.op).trW s') (fac : s.op ≫ b = s'),
    ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
⊢ ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

Tactic:
obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff])

Premises used: Quiver.Hom.op
-- 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.op X → B.op.trW s → ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
Z' : Cᵒᵖ
s' : op Y ⟶ Z'
b : op X ⟶ Z'
hZ' : A.op Z'
hs' : (A.op ⊓ B.op).trW s'
fac : s.op ≫ b = s'
⊢ ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

Tactic:
exact ⟨Z'.unop, s'.unop, b.unop, hZ', trW_of_op _ hs', 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
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
X Y : Cᵒᵖ
s : X ⟶ Y
hX : A.op X
hs : B.op.trW s
refine_2 :
  ∀ (Z' : C) (s' : Z' ⟶ unop X) (b : Z' ⟶ unop Y) (hZ' : A Z') (hs' : (A ⊓ B).trW s') (fac : b ≫ s.unop = s'),
    ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
⊢ ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs)

Premises used: Quiver.Hom.unop, CategoryTheory.ObjectProperty.trW_of_op
-- 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 Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
X Y : Cᵒᵖ
s : X ⟶ Y
hX : A.op X
hs : B.op.trW s
Z' : C
s' : Z' ⟶ unop X
b : Z' ⟶ unop Y
hZ' : A Z'
hs' : (A ⊓ B).trW s'
fac : b ≫ s.unop = s'
⊢ ∃ (Z : Cᵒᵖ) (s' : X ⟶ Z) (b : Y ⟶ Z), A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'

Tactic:
exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', 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
inst_9 : A.IsVerdierLeftLocalizing B
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
⊢ ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

Tactic:
(isVerdierLeftLocalizing_iff A B).1 inferInstance s hY hs

Premises used: CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_iff, inferInstance, Iff.mp
-- 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 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
hf : (B.inverseImage A.ι).trW f
⊢ ∃ (Z : A.FullSubcategory) (g : Y ⟶ Z) (h :
    Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor A.FullSubcategory (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
      (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _) (Triangle.mk f g h)),
    B.inverseImage A.ι Z

Tactic:
simp only [MorphismProperty.inverseImage_iff, trW_iff] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.inverseImage_iff, CategoryTheory.ObjectProperty.trW_iff
-- 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 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
hf :
  ∃ (Z : A.FullSubcategory) (g : Y ⟶ Z) (h :
    Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor A.FullSubcategory (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
      (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _) (Triangle.mk f g h)),
    B.inverseImage A.ι Z
obtain :
  ∀ (Z : A.FullSubcategory) (a : Y ⟶ Z)
    (b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor A.FullSubcategory (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
        (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _) (Triangle.mk f a b))
    (hZ : B.inverseImage A.ι Z),
    ∃ (Z : C) (g : A.ι.obj Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (A.ι.obj X)) (_
      :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_4 _ inst_6 inst_7 _) (Triangle.mk (A.ι.map f) g h)),
      B Z
⊢ ∃ (Z : C) (g : A.ι.obj Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (A.ι.obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_4 _ inst_6 inst_7 _) (Triangle.mk (A.ι.map f) g h)),
    B Z

Tactic:
obtain ⟨Z, a, b, hT, hZ⟩ := hf
-- 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 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : A.FullSubcategory
a : Y ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor A.FullSubcategory (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _) (Triangle.mk f a b)
hZ : B.inverseImage A.ι Z
⊢ ∃ (Z : C) (g : A.ι.obj Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (A.ι.obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_4 _ inst_6 inst_7 _) (Triangle.mk (A.ι.map f) g h)),
    B Z

Tactic:
⟨_, _, _, A.ι.map_distinguished _ hT, hZ⟩

Premises used: CategoryTheory.ObjectProperty.ι, Exists.intro, CategoryTheory.Functor.map_distinguished
-- 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 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : A.FullSubcategory
a : Y ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor A.FullSubcategory (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _) (Triangle.mk f a b)
hZ : B.inverseImage A.ι Z
⊢ ∃ (Z : C) (g : A.ι.obj Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (A.ι.obj X)) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_4 _ inst_6 inst_7 _) (Triangle.mk (A.ι.map f) g h)),
    B Z

Tactic:
exact ⟨_, _, _, A.ι.map_distinguished _ hT, hZ⟩
-- 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 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : A.IsTriangulated
⊢ (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
      (A.triangulatedLocalizerMorphism B)).IsTriangulated

Tactic:
inferInstanceAs A.ι.IsTriangulated

Premises used: _private.0.CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphism._proof_1