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.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 : 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
refine : ∀ (X₁ X₂ : A.FullSubcategory) (f : X₁ ⟶ X₂) (hf : F.map (L₁.map f) = 0), L₁.map f = 0
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Faithful

Tactic:
refine Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions L₁
    (B.inverseImage A.ι).trW F (fun X₁ X₂ f hf ↦ ?_)

Premises used: CategoryTheory.Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions, CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.trW, 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.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 : 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₂
hf : F.map (L₁.map f) = 0
⊢ L₂.map f.hom = L₂.map 0

Tactic:
simp [← dsimp% NatIso.naturality_2 e f, hf]

Premises used: CategoryTheory.NatIso.naturality_2
-- 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
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 : 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₂
hf : F.map (L₁.map f) = 0
⊢ L₂.map f.hom = L₂.map 0

Tactic:
replace hf : L₂.map f.hom = L₂.map 0 := by
    simp [← dsimp% NatIso.naturality_2 e f, hf]
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : 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 : 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₂
hf : L₂.map f.hom = L₂.map 0
⊢ ∃ (Z : C) (s : X₂.obj (P := A) ⟶ Z) (_ : B.trW s), f.hom ≫ s = 0 ≫ s

Tactic:
rw [MorphismProperty.map_eq_iff_postcomp L₂ B.trW] at hf

Premises used: CategoryTheory.MorphismProperty.map_eq_iff_postcomp, CategoryTheory.ObjectProperty.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
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 : 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₂
hf : ∃ (Z : C) (s : X₂.obj (P := A) ⟶ Z) (_ : B.trW s), f.hom ≫ s = 0 ≫ s
obtain : ∀ (X₃ : C) (s : X₂.obj (P := A) ⟶ X₃) (hs : B.trW s) (fac : f.hom ≫ s = 0 ≫ s), L₁.map f = 0
⊢ L₁.map f = 0

Tactic:
obtain ⟨X₃, s, hs, fac⟩ := hf
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : 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 : 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
obtain :
  ∀ (X₄ : C) (t : X₂.obj (P := A) ⟶ X₄) (a : X₃ ⟶ X₄) (hX₄ : A X₄) (ht : (A ⊓ B).trW t) (fac' : s ≫ a = t), L₁.map f = 0
⊢ L₁.map f = 0

Tactic:
obtain ⟨X₄, t, a, hX₄, ht, fac'⟩ :=
    IsVerdierRightLocalizing.fac' s X₂.property hs

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac'
-- 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
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 : 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
rwa rwa₁ rwa₂ rwa₃ : (A ⊓ B).trW t'.hom
⊢ (B.inverseImage A.ι).trW t'

Tactic:
rwa [trW_inverseImage_ι_iff]

Premises used: CategoryTheory.ObjectProperty.trW_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.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 : 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
⊢ IsIso (L₁.map t')

Tactic:
have := Localization.inverts L₁ (B.inverseImage A.ι).trW t'
    (by rwa [trW_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.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')
rw : L₁.map (f ≫ t') = L₁.map 0
⊢ L₁.map f = 0

Tactic:
rw [← cancel_mono (L₁.map t'), zero_comp, ← L₁.map_comp, ← L₁.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp
-- 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
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')
e_a : f ≫ t' = 0
⊢ L₁.map (f ≫ t') = L₁.map 0

Tactic:
congr 1
-- 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
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')
e_a : (f ≫ t').hom = InducedCategory.Hom.hom 0
⊢ f ≫ t' = 0

Tactic:
ext
-- 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
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').hom = InducedCategory.Hom.hom 0

Tactic:
simp [t', ← fac', reassoc_of% fac]
-- 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) }
rw : L₂.op.IsLocalization B.trW.op
⊢ L₂.op.IsLocalization B.op.trW

Tactic:
rw [trW_op]

Premises used: CategoryTheory.ObjectProperty.trW_op