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 : 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
this_1 : Preadditive.{v_3, u_3} D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this_2 : Preadditive.{v_4, u_4} D₂ := Localization.preadditive L₂ B.trW
this_3 : L₁.Additive
this_4 : L₂.Additive
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₂
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 : X₁ ⟶ X₂
X₃ : C
s : X₂.obj (P := A) ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj (P := A) ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ FullSubcategory.mk (P := A) X₄ hX₄ := homMk (P := A) t
this : IsIso (L₁.map t')
⊢ L₁.map f = 0
have rw : L₁.map (f ≫ t') = L₁.map 0
Tactic: rw [← cancel_mono (L₁.map t'), zero_comp, ← L₁.map_comp, ← L₁.map_zero]
-- 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
this_1 : Preadditive.{v_3, u_3} D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this_2 : Preadditive.{v_4, u_4} D₂ := Localization.preadditive L₂ B.trW
this_3 : L₁.Additive
this_4 : L₂.Additive
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₂
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 : X₁ ⟶ X₂
X₃ : C
s : X₂.obj (P := A) ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj (P := A) ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ FullSubcategory.mk (P := A) X₄ hX₄ := homMk (P := A) t
this : IsIso (L₁.map t')
⊢ L₁.map (f ≫ t') = L₁.map 0
have e_a : f ≫ t' = 0
Tactic: congr 1
-- 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
this_1 : Preadditive.{v_3, u_3} D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this_2 : Preadditive.{v_4, u_4} D₂ := Localization.preadditive L₂ B.trW
this_3 : L₁.Additive
this_4 : L₂.Additive
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₂
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 : X₁ ⟶ X₂
X₃ : C
s : X₂.obj (P := A) ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj (P := A) ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ FullSubcategory.mk (P := A) X₄ hX₄ := homMk (P := A) t
this : IsIso (L₁.map t')
⊢ f ≫ t' = 0
have e_a : (f ≫ t').hom = InducedCategory.Hom.hom 0
Tactic: ext
-- 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.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
have rw : L₂.op.IsLocalization B.trW.op
Tactic: rw [trW_op]
-- 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.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) }
⊢ LocalizerMorphism.IsLocalizedFullyFaithful (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
    (A.triangulatedLocalizerMorphism B)
have this₁ : L₂.op.IsLocalization B.op.trW
Tactic: have : L₂.op.IsLocalization B.op.trW := by rw [trW_op]; infer_instance
-- 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.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.ι))
have refine_1 : (B.inverseImage A.ι).trW.op ≤
  MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
    A.opEquivalence.symm.functor
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 _)
-- 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.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
⊢ (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))
have refine_2 : MorphismProperty.IsInvertedBy (trW (B.op.inverseImage A.op.ι)) (A.opEquivalence.functor ⋙ L₁.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 _)
-- 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.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
⊢ (B.inverseImage A.ι).trW.op ≤
    MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
      A.opEquivalence.symm.functor
have 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
Tactic: rw [← trW_op, ← inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op]
-- 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.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
⊢ MorphismProperty.inverseImage (MorphismProperty.isoClosure (trW (B.op.inverseImage A.op.ι)))
    A.opEquivalence.symm.functor f
have hf₁ : trW (B.op.inverseImage A.op.ι) (A.opEquivalence.inverse.map f)
Tactic: simp only [MorphismProperty.inverseImage_iff, Equivalence.symm_functor] at hf ⊢
Cleared hypotheses: hf
-- 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.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)
have 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)
Tactic: refine fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_
-- 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.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
⊢ LocalizerMorphism.IsLocalizedFullyFaithful (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
    (A.triangulatedLocalizerMorphism B)
have this₁ : (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))
Tactic: have : (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (B.op.inverseImage A.op.ι).trW := by
    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 _)
    · rw [← trW_op, ← inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op]
      intro _ _ f hf
      simp only [MorphismProperty.inverseImage_iff, Equivalence.symm_functor] at hf ⊢
      exact MorphismProperty.le_isoClosure _ _ hf
    · refine fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_
      simpa [trW_inverseImage_ι_iff, ← op_inf, trW_op] using hf
-- 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.IsVerdierLeftLocalizing 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
inst_16 : A.IsVerdierLeftLocalizing B
inst_17 : Preadditive.{v_3, u_3} D₁
inst_18 : Preadditive.{v_4, u_4} D₂
inst_19 : L₁.Additive
inst_20 : L₂.Additive
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₂).Additive
have rw : (L₁ ⋙
    LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
      (A.triangulatedLocalizerMorphism B) L₁ L₂).Additive
Tactic: rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
⊢ adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
have h : ∀ (x : Dᵒᵖ),
  adj.op.unit.app x =
    NatTrans.app
      (Adjunction.unit
        (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) sorry) (OppositeShift.adjunction ℤ adj)))
      x
Tactic: ext