awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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
⊢ ∃ (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
have 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 _ _ sorry _ (Preadditive.fullSubcategory A) sorry _) (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: obtain ⟨Z, a, b, hT, hZ⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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) (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
have 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 _ _ sorry _ (Preadditive.fullSubcategory A) sorry _) (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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
⊢ (∃ (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
have 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 _ _ sorry _ (Preadditive.fullSubcategory A) sorry _) (Triangle.mk f g h)),
    B.inverseImage A.ι Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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
have mpr : Membership.mem (γ := Set (Triangle.{v_1, u_1} A.FullSubcategory))
  (@Pretriangulated.distinguishedTriangles _ _ sorry _ (Preadditive.fullSubcategory A) sorry _)
  (Triangle.mk (Z := FullSubcategory.mk (P := A) Z sorry) f (homMk (P := A) a)
    (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X)))
Tactic: refine ⟨⟨Z, hZ.1⟩, A.homMk a, A.homMk (b ≫ (A.ι.commShiftIso 1).inv.app _), ?_, hZ.2⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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} 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)))
have 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 sorry) f (homMk (P := A) a)
      (homMk (P := A) (b ≫ NatTrans.app (Iso.inv (Functor.commShiftIso A.ι 1)) X))))
Tactic: rw [← A.ι.map_distinguished_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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))))
have mpr : Triangle.mor₁
      (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
        (Triangle.mk (Z := FullSubcategory.mk (P := A) Z sorry) 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 sorry) 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 sorry) 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: refine isomorphic_distinguished _ h _
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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 :
  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)))) ≫
      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₁
⊢ 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))))
have mpr₁ : Triangle.mor₂
      (Functor.obj (C := Triangle.{v_1, u_1} A.FullSubcategory) A.ι.mapTriangle
        (Triangle.mk (Z := FullSubcategory.mk (P := A) Z sorry) 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 sorry) 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 sorry) 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: refine isomorphic_distinguished _ h _
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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
⊢ MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse = (B.inverseImage A.ι).op.trW
have 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
Tactic: ext ⟨X₁⟩ ⟨X₂⟩ a
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (hypothesis)
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₂
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Full
have this : L₁.EssSurj
Tactic: have : L₁.EssSurj := Localization.essSurj L₁ (B.inverseImage A.ι).trW
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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
have 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 = φ
Tactic: refine F.full_of_comp_essSurj L₁ (fun X₁ X₂ φ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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₂)
⊢ ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
have 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 = φ
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]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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₂
⊢ ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
have obtain : ∀ (f : B.trW.LeftFraction (A.ι.obj X₁) (A.ι.obj X₂)) (hf : φ' = f.map (W := B.trW) L₂ sorry),
  ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
Tactic: obtain ⟨f, hf⟩ := Localization.exists_leftFraction L₂ B.trW φ'
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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₂
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 = φ
have obtain : ∀ (X₃ : C) (s' : A.ι.obj X₂ ⟶ X₃) (a : f.Y' (W := B.trW) ⟶ X₃) (hX₃ : A X₃) (hs' : (A ⊓ B).trW s')
  (fac : f.s (W := B.trW) ≫ a = s'), ∃ (f : L₁.obj X₁ ⟶ L₁.obj X₂), F.map f = φ
Tactic: obtain ⟨X₃, s', a, hX₃, hs', fac⟩ :=
    IsVerdierRightLocalizing.fac' f.s X₂.property f.hs