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
X Y : A.FullSubcategory
f : X ⟶ Y
mp :
  (∃ (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) →
    ∃ (Z : C) (g : Y.obj (P := A) ⟶ Z) (h :
      Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom g h)),
      (A ⊓ B) Z
mpr :
  (∃ (Z : C) (g : Y.obj (P := A) ⟶ Z) (h :
      Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom g h)),
      (A ⊓ B) Z) →
    ∃ (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
⊢ (∃ (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) ↔
    ∃ (Z : C) (g : Y.obj (P := A) ⟶ Z) (h :
      Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))) (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
        (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom g h)),
      (A ⊓ B) Z

Tactic:
constructor
-- 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
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
h :
  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 : Y.obj (P := A) ⟶ Z) (h :
    Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom g h)),
    (A ⊓ B) Z

Tactic:
⟨_, _, _, A.ι.map_distinguished _ h, Z.property, hZ⟩

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.FullSubcategory.property, And.intro, Exists.intro, CategoryTheory.Functor.map_distinguished
-- 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
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
h :
  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 : Y.obj (P := A) ⟶ Z) (h :
    Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
      (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom g h)),
    (A ⊓ B) Z

Tactic:
exact ⟨_, _, _, A.ι.map_distinguished _ h, Z.property, hZ⟩
-- 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
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj (P := A) ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom a b)
hZ : (A ⊓ B) Z
⊢ ∃ (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:
⟨⟨Z, hZ.1⟩, A.homMk a, A.homMk (b ≫ (A.ι.commShiftIso 1).inv.app _), ?_, hZ.2⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ι, And.right, And.left, CategoryTheory.ObjectProperty.homMk, Exists.intro, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- 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
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj (P := A) ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom a b)
hZ : (A ⊓ B) Z
mpr :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _)
    (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
      (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X)))
⊢ ∃ (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:
refine ⟨⟨Z, hZ.1⟩, A.homMk a, A.homMk (b ≫ (A.ι.commShiftIso 1).inv.app _), ?_, hZ.2⟩
-- 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
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj (P := A) ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom a b)
hZ : (A ⊓ B) Z
mpr :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
      (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
        (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X))))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory A) ⋯ _)
    (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
      (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X)))

Tactic:
rw [← A.ι.map_distinguished_iff]

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.map_distinguished_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
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj (P := A) ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom a b)
hZ : (A ⊓ B) Z
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
      (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
        (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X))))

Tactic:
isomorphic_distinguished _ h _
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Pretriangulated.isomorphic_distinguished
-- 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
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj (P := A) ⟶ Z
b : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.obj (P := A))
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f.hom a b)
hZ : (A ⊓ B) Z
⊢ Triangle.mor₃
        (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
          (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
            (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X)))) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom
          (Iso.refl
            (Triangle.obj₁
              (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
                (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
                  (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X))))))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₃
            (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
              (Triangle.mk (Z := FullSubcategory.mk (P := A) Z ⋯) f (homMk (P := A) a)
                (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X)))))) ≫
      (Triangle.mk f.hom a b).mor₃

Tactic:
simp [dsimp% (A.ι.commShiftIso (1 : ℤ)).inv_hom_id_app X]

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Iso.inv_hom_id_app, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso
-- 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 :
  ∀ (X₁ X₂ : A.FullSubcategory) (a : op X₁ ⟶ op X₂),
    MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse a ↔
      (B.inverseImage A.ι).op.trW a
⊢ MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse = (B.inverseImage A.ι).op.trW

Tactic:
ext ⟨X₁⟩ ⟨X₂⟩ a
-- 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₁ X₂ : A.FullSubcategory
a : op X₁ ⟶ op X₂
⊢ MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse a ↔
    (B.inverseImage A.ι).op.trW a

Tactic:
simp [trW_op, trW_inverseImage_ι_iff, ← op_inf]

Premises used: CategoryTheory.ObjectProperty.trW_inverseImage_ι_iff, CategoryTheory.ObjectProperty.op_inf, CategoryTheory.ObjectProperty.trW_op
-- 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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierRightLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
⊢ L₁.EssSurj

Tactic:
have : L₁.EssSurj := Localization.essSurj L₁ (B.inverseImage A.ι).trW
-- 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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierRightLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Full

Tactic:
F.full_of_comp_essSurj L₁ (fun X₁ X₂ φ ↦ ?_)

Premises used: CategoryTheory.Functor.full_of_comp_essSurj
-- 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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierRightLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
refine :
  ∀ (X₁ X₂ : A.FullSubcategory) (φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)), ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Full

Tactic:
refine F.full_of_comp_essSurj L₁ (fun X₁ X₂ φ ↦ ?_)

Premises used: CategoryTheory.Functor.full_of_comp_essSurj
-- 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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierRightLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
⊢ φ = e.inv.app X₁ ≫ (e.hom.app X₁ ≫ φ ≫ e.inv.app X₂) ≫ e.hom.app X₂

Tactic:
simp [dsimp% e.inv_hom_id_app_assoc, dsimp% e.inv_hom_id_app]

Premises used: CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc
-- 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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierRightLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
obtain :
  ∀ (φ' : (A.ι ⋙ L₂).obj X₁ ⟶ (A.ι ⋙ L₂).obj X₂) (hφ' : φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂),
    ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
⊢ ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ

Tactic:
obtain ⟨φ', hφ'⟩ : ∃ φ', φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂ :=
    ⟨e.hom.app X₁ ≫ φ ≫ e.inv.app X₂, by
      simp [dsimp% e.inv_hom_id_app_assoc, dsimp% e.inv_hom_id_app]⟩

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- 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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierRightLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
φ' : (A.ι ⋙ L₂).obj X₁ ⟶ (A.ι ⋙ L₂).obj X₂
hφ' : φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂
obtain :
  ∀ (f : B.trW.LeftFraction (A.ι.obj X₁) (A.ι.obj X₂)) (hf : φ' = f.map (W := B.trW) L₂ ⋯),
    ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
⊢ ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ

Tactic:
obtain ⟨f, hf⟩ := Localization.exists_leftFraction L₂ B.trW φ'

Premises used: CategoryTheory.Localization.exists_leftFraction, CategoryTheory.ObjectProperty.trW