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 : 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
⊢ L₂.op.IsLocalization B.trW.op

Tactic:
infer_instance
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
⊢ L₂.op.IsLocalization B.op.trW

Tactic:
have : L₂.op.IsLocalization B.op.trW := by rw [trW_op]; infer_instance
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))

Tactic:
Functor.IsLocalization.of_equivalence_source L₁.op (B.inverseImage A.ι).trW.op
      _ _ A.opEquivalence.symm ?_ ?_
      ((Functor.associator _ _ _).symm ≪≫
        Functor.isoWhiskerRight A.opEquivalence.counitIso _ ≪≫ Functor.leftUnitor _)

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.associator, CategoryTheory.MorphismProperty.op, CategoryTheory.Functor.IsLocalization.of_equivalence_source, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.ObjectProperty.trW, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.opEquivalence, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.ObjectProperty.inverseImage, CategoryTheory.Equivalence.symm, CategoryTheory.Equivalence.counitIso
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
refine_1 :
  (B.inverseImage A.ι).trW.op ≤
    MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
      A.opEquivalence.symm.functor
refine_2 : MorphismProperty.IsInvertedBy (trW (B.op.inverseImage A.op.ι)) (A.opEquivalence.functor ⋙ L₁.op)
⊢ (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))

Tactic:
refine Functor.IsLocalization.of_equivalence_source L₁.op (B.inverseImage A.ι).trW.op
      _ _ A.opEquivalence.symm ?_ ?_
      ((Functor.associator _ _ _).symm ≪≫
        Functor.isoWhiskerRight A.opEquivalence.counitIso _ ≪≫ Functor.leftUnitor _)

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.associator, CategoryTheory.MorphismProperty.op, CategoryTheory.Functor.IsLocalization.of_equivalence_source, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.ObjectProperty.trW, CategoryTheory.Iso.symm, CategoryTheory.ObjectProperty.opEquivalence, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.ObjectProperty.inverseImage, CategoryTheory.Equivalence.symm, CategoryTheory.Equivalence.counitIso
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
refine_1 :
  MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse ≤
    MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
      A.opEquivalence.symm.functor
⊢ (B.inverseImage A.ι).trW.op ≤
    MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
      A.opEquivalence.symm.functor

Tactic:
rw [← trW_op, ← inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op]

Premises used: CategoryTheory.ObjectProperty.trW_op, CategoryTheory.ObjectProperty.inverseImage_opEquivalence_inverse_trW_inverseImage_ι_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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
X : A.FullSubcategoryᵒᵖ
refine_1 :
  ∀ ⦃Y : A.FullSubcategoryᵒᵖ⦄ (f : X ⟶ Y),
    MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse f →
      MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
        A.opEquivalence.symm.functor f
⊢ ∀ ⦃Y : A.FullSubcategoryᵒᵖ⦄ (f : X ⟶ Y),
    MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse f →
      MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
        A.opEquivalence.symm.functor f

Tactic:
_
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
X Y : A.FullSubcategoryᵒᵖ
f : X ⟶ Y
hf : MorphismProperty.inverseImage (trW (B.op.inverseImage A.op.ι)) A.opEquivalence.inverse f
⊢ trW (B.op.inverseImage A.op.ι) (A.opEquivalence.inverse.map f)

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

Premises used: CategoryTheory.Equivalence.symm_functor, CategoryTheory.MorphismProperty.inverseImage_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 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
X Y : A.FullSubcategoryᵒᵖ
f : X ⟶ Y
hf : trW (B.op.inverseImage A.op.ι) (A.opEquivalence.inverse.map f)
⊢ MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)) (A.opEquivalence.inverse.map f)

Tactic:
MorphismProperty.le_isoClosure _ _ hf

Premises used: CategoryTheory.MorphismProperty.le_isoClosure
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
X Y : A.FullSubcategoryᵒᵖ
f : X ⟶ Y
hf : trW (B.op.inverseImage A.op.ι) (A.opEquivalence.inverse.map f)
⊢ MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)) (A.opEquivalence.inverse.map f)

Tactic:
exact MorphismProperty.le_isoClosure _ _ hf

Premises used: CategoryTheory.MorphismProperty.le_isoClosure
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ MorphismProperty.IsInvertedBy (trW (B.op.inverseImage A.op.ι)) (A.opEquivalence.functor ⋙ L₁.op)

Tactic:
fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.ι, Quiver.Hom.op, CategoryTheory.Equivalence.functor, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.IsInvertedBy, CategoryTheory.Functor.map, CategoryTheory.ObjectProperty.trW, CategoryTheory.ObjectProperty.opEquivalence, CategoryTheory.Localization.inverts, CategoryTheory.ObjectProperty.inverseImage
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
refine_2 :
  ∀ (x x_1 : FullSubcategory.{v_1, u_1} A.op) (x_2 : x ⟶ x_1) (hf : trW (B.op.inverseImage A.op.ι) x_2),
    (B.inverseImage A.ι).trW.op (A.opEquivalence.functor.map x_2)
⊢ MorphismProperty.IsInvertedBy (trW (B.op.inverseImage A.op.ι)) (A.opEquivalence.functor ⋙ L₁.op)

Tactic:
refine fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_

Premises used: CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.ι, CategoryTheory.MorphismProperty.op, CategoryTheory.ObjectProperty.trW, CategoryTheory.Localization.inverts, CategoryTheory.ObjectProperty.inverseImage
-- 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.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
x x_1 : FullSubcategory.{v_1, u_1} A.op
x_2 : x ⟶ x_1
hf : trW (B.op.inverseImage A.op.ι) x_2
⊢ (B.inverseImage A.ι).trW.op (A.opEquivalence.functor.map x_2)

Tactic:
simpa [trW_inverseImage_ι_iff, ← op_inf, trW_op] using hf

Premises used: CategoryTheory.ObjectProperty.trW_inverseImage_ι_iff, CategoryTheory.ObjectProperty.op_inf, CategoryTheory.ObjectProperty.trW_op